# Types and Semantics for Programming Languages

## Schedule

10.00–10.50 Monday (lecture)
11.10–12.00 Monday (tutorial)
10.00–10.50 Thursday (lecture)
11.10–12.00 Thursday (tutorial)
10.00–10.50 Friday (lecture)
11.10–12.00 Friday (tutorial)

All lectures and tutorials in AT 5.08.

Note: Lectures begin Monday of Week 1.

## Assignments

Coursework is worth 25% of your mark. There are five coursework assignments, each worth 5%.

For each assignment you will be given a list of exercises to complete in the textbook. Copy the relevant files and fill in your answers. Include a comment at the beginning, listing your name and which exercises you completed. Mark every completed exercise by writing `(* !!! *)` just before it. E-mail your files to the instructor. Send all relevant files: .v, .vo, and .glob. Please ensure your files execute correctly under Coq!

Some exercises are labeled 'stretch'. These are optional exercises for students who wish an additional challenge.

Note: The coursework is not a light load! But everyone who does the work gets perfect on the exam. (Literally. 100%. That's what proof is for.)

• Assignment 1. Due 4pm Thursday 28 September 2017 (Week 2).
• Basics (`Basics.v`):
• `factorial`
• `blt_nat`, defined in terms of previously given functions.
• `blt_nat'`, this time defined directly using recursion.
• `andb_eq_orb`
• `binary` (stretch)
• Induction (`Induction.v`):
• `double_plus`
• Prove `Theorem plus_swap : forall m n p, n + (m + p) = m + (n + p).` (Hint: this requires only `plus_assoc` and `plus_comm`.)
• Prove `Theorem mult_S_r : forall m n, m * S n = m + (m * n).`
• Prove `Theorem mult_comm : forall m n, m * n = n * m.`
• Prove `Theorem beq_nat_refl : forall n, beq_nat n n = true.`
• If you've done `binary`, prove `Theorem binary_comm : forall b, bin_to_nat (incr b) = S (bin_to_nat b).` (stretch)
• Lists (`Lists.v`):
• `list_funs`
• `list_exercises`
• `update_eq` (stretch)
• `update_neq` (stretch)
• Assignment 2. Due 4pm Thursday 12 October (Week 4).
• Poly (`Poly.v`):
• `poly_exercises`: `app_length`
• `more_poly_exercises`
• `fold_length`
• Tactics (`Tactics.v`):
• `beq_nat_true`
• `beq_nat_sym`
• `beq_nat_trans` (stretch)
• `forall_exists_challenge` (stretch)
• Logic (`Logic.v`):
• `contrapositive`
• `not_both_true_and_false`
• `or_distributes_over_and`
• `dist_not_exists`
• `not_exists_dist` (stretch)
• `classical_axioms` (stretch)
• IndProp (`IndProp.v`):
• `le_exercises`, first five theorems:
• `le_trans`
• `O_le_n`
• `n_le_m__Sn_le_Sm`
• `Sn_le_Sm__n_le_m`
• `le_plus_l`
• `palindromes` (stretch)
• Assignment 3. Due 4pm Thursday 26 October 2017 (Week 6).
• Maps (`Maps.v`):
• `t_update_shadow`
• `t_update_permute` (stretch)
• Imp (`Imp.v`).
• `ceval_example2`
• `extend_repeat`
Make a copy of the semantics of the imperative language, and extend it with a construct
`REPEAT c UNTIL b END`
that is equivalent to
`c ;; WHILE ~b DO c END`
where `~b` is the logical negation of `b`. Put the copy in a nested module called `extend_repeat`, so that you can reuse all the constructor names.
• `bevalR`
• `no_whiles_terminating`
• `stack_compiler` (stretch)
• `stack_compiler_correct` (stretch) -->
• Equiv (`Equiv.v`):
• `swap_if_branches`
• `assign_aequiv`
• `CIf_congruence`
• `fold_constants_com_sound` (stretch)
• Hoare (`Hoare.v`):
• `swap_exercise`
• `hoare_repeat`
Prove the following for the `REPEAT` construct introduced earlier.
``` {{P}}c{{Q}}    Q /\ ~b ->> P ------------------------------------- {{P}}REPEAT b UNTIL c END{{Q /\ b}} ```
• Hoare2 (`Hoare2.v`)
• `factorial`
• `factorial_dec` (stretch)
• Assignment 4. Due 4pm Thursday 9 November (Week 8).
• Smallstep (`Smallstep.v`):
• `eval__multistep`
• `step__eval` (stretch)
• `multistep__eval` (stretch)
• `par_body_n__Sn`
• `par_body_n` (stretch)
• Types (`Types.v`)
• Stlc (`Stlc.v`):
• `step_example5`
• `typing_example2_full`
• StlcProp (`StlcProp.v`):
• `types_unique` (stretch)
• `progress_preservation_statement`
• MoreStlc (`MoreStlc.v`):
• `halve_fix`
Write out your solution informally. After you've completed `STLC_extensions`, you can write it out formally.
• `STLC_extensions` You are provided with the implementations for
• Numbers
• Sums
• Lists
• Unit (the identity for pairs)
You need to complete the implementations for:
• Pairs
• Let (which involves binding)
• Fix
• Empty (the identity for sums)
The rules for the Empty type are:
• Types: `T ::= ... | Empty`
• Terms: `t ::= ... | case t of {}`
• Values: there are no values of empty type
• Reduction rules:
``` t ==> t' -------------------------------- case t of {} ==> case t' of {} ```
• Type rules:
``` Gamma |- t : Empty ------------------------- Gamma |- case t of {} : T ```
NB: types are not unique!
[Added clarification: Please be sure to fill in all occurrences of `Admitted` in any lemmas or theorems on which you depend. In particular, for STLC_extensions you will need to complete the following:
• ty
• tm
• subst
• step
• has_type
• progress
• appears_free_in
• context_invariance
• free_in_context
• substitution_preserves_typing
• preservation
You might also want to prove new canonical form lemmas.]
• Typechecking (`Typechecking.v`):
• `typechecker_extensions` (stretch)
Extend the typechecker to support any of the extensions in `STLC_extensions`.
• Assignment 5. Due 4pm Thursday 23 November (Week 10). Mock exam.
• Mock exam Do all three questions. The mock exam copies the rubric of the real exam, which requires you to do two out of three questions.
• Exam.v
• Maps.v

## Second mock exam

• Second mock exam: 10am–12noon Thursday 30 November (Week 11).

## Good scholarly practice

Furthermore, you are required to take reasonable measures to protect your assessed work from unauthorised access. For example, if you put any such work on a public repository then you must set access permissions appropriately (generally permitting access only to yourself, or your group in the case of group practicals).

## Lecture log

• Monday 18 September 2017 (Week 1)
• Lecture:
• ICFP 2017
• Assignment schedule, December examination.
• Basics (`Basics.v`):
• `Nat`, `plus`, `mult`
• `Bool`, `negb`, `andb`
• `beq_nat`, `leb`
• Tutorial:
• Basics (`Basics.v`):
• `factorial`
• `blt_nat`, defined in terms of previously given functions.
• `blt_nat'`, this time defined directly using recursion.
• Friday 22 September 2017 (Week 1)
• Lecture:
• Induction (`Induction.v`):
• Compile `Basics.v` to `Basics.vo`
• Proof by induction `induction`, proof by cases `destruct`
• `plus_n_O`
• `plus_n_Sm`
• `plus_comm`
• `plus_assoc`
• Tutorial:
• Induction (`Induction.v`):
• `double_plus`
• Prove `Theorem plus_swap : forall m n p, n + (m + p) = m + (n + p).` (Hint: this requires only `plus_assoc` and `plus_comm`.)
• Prove `Theorem mult_S_r : forall m n, m * S n = m + (m * n).`
• Prove `Theorem mult_comm : forall m n, m * n = n * m.`
• Monday 25 September 2017 (week 2)
• Thursday 28 September 2017 (week 2)
• Lecture:
• Poly (`Poly.v`)
• `list X`, `repeat`
• type inference, argument synthesis, implicit arguments
• `app`, `length`
• `map`, `map_rev`, `filter`
• `option`, `nth_error`
• Tutorial:
• Any not done from Assignment 1
• Poly (`Poly.v`):
• `poly_exercises`: `app_length`
• `more_poly_exercises`
• Friday 29 September 2017 (week 2)
• Lecture:
• Tactics (`Tactics.v`):
• `inversion`
• Varying the induction hypothesis
• `double_injective`
• `generalise dependent`
• Review these sections, covered in class
• The inversion tactic
• Varying the induction hypothesis
• Study the following sections on your own
• The apply tactic
• The apply ... with ... tactic
• Using tactics on hypotheses
• Unfolding definitions
• Applying destruct on compound definitions
• Review
• Tutorial:
• Monday 2 October 2017 (week 3)
• Lecture:
• Logic (`Logic.v`):
• Proof rules come in pairs, introduction (how do I show A holds?) and elimination (assuming A holds, how can I use it?)
• Implication: intro `intro`, elim `apply`
• Conjunction: intro `split`, elim `destruct H as [HA HB]`
• Disjunction: intro `left`, `right`, elim `destruct H as [HA|HB]`
• True: into `I`, elim not possible.
• False: intro not possible, elim `destruct H as []` or `exfalso`
• Negation: `unfold` and then as for implication
• Propositions as Types, further notes here: `PaT.v`.
• Tutorial:
• Thursday 5 October 2017 (week 3)
• Lecture:
• Logic (`Logic.v`):
• Logical equivalence: as for conjunction and implication
• Universal quantification: intro `intro`, elim `apply`
• Existential quantification: intro `exists`, elim `destruct H as [x H']`
• Classical vs constructive (intuitionistic) logic
• Tutorial:
• Logic (`Logic.v`):
• `contrapositive`
• `not_both_true_and_false`
• `dist_not_exists`
• `beq_nat_false_iff`
• `not_exists_dist` (stretch)
• `classical_axioms` (stretch)
• Friday 6 October 2017 (week 3)
• Lecture:
• IndProp (`IndProp.v`):
• Inductively Defined Propositions: `ev`, `ev_double`
• Inversion on Evidence: `evSS_ev`
• Induction over Evidence: `ev_even`, `ev_even_iff`
• Inductive Relations: `le`, `0_le_n`, `total_relation`, `empty_relation`
• Tutorial:
• IndProp (`IndProp.v`):
• `le_exercises`, first five theorems:
• `le_trans`
• `O_le_n`
• `n_le_m__Sn_le_Sm`
• `Sn_le_Sm__n_le_m`
• `le_plus_l`
• `palindromes` (stretch)
• Monday 9 October 2017 (week 4)
• Lecture:
• Maps (`Maps.v`)
• Rel (`Rel.v`)
• Imp (`Imp.v`):
• Arithmetic and Boolean Expressions: `aexp`, `bexp`, `aeval`, `beval`
• Evaluation as a Relation: `aevalR`, `aeval_iff_aevalR`
• Expressions With Variables: `aeval`, `beval`
• Commands: `com`
• Evaluation as a Function (Failed Attempt): `ceval_fun_no_while`
• Evaluation as a Relation: `ceval`
• Tutorial:
• Imp (`Imp.v`):
• `ceval_example2`
• `extend_repeat`
Make a copy of the semantics of the imperative language, and extend it with a construct
`REPEAT c UNTIL b END`
that is equivalent to
`c ;; WHILE ~b DO c END`
where `~b` is the logical negation of `b`. Put the copy in a nested module called `extend_repeat`, so that you can reuse all the constructor names.
• `bevalR`
• `no_whiles_terminating`
• `stack_compiler` (stretch)
• `stack_compiler_correct` (stretch)
• Thursday 12 October (week 4)
• Lecture:
• Equiv (`Equiv.v`):
• How `eapply` works. See "Digression: The eapply Tactic" in the next chapter.
• Behavioral Equivalence: `aequiv`, `bequiv`, `cequiv`
• Examples: `skip_left`, `IFB_true`, `WHILE_true_nonterm`
• The Functional-Extensionality Axiom: `functional_extensionality`
• Behavioral Equivalence is an Equivalence
• Behavioral Equivalence is a Congruence: `CWhile_congruence`
• Tutorial:
• Equiv (`Equiv.v`):
• `swap_if_branches`
• `assign_aequiv`
• `CIf_congruence`
• `fold_constants_com_sound` (stretch)
• Friday 13 October 2017 (week 4)
• Lecture:
• Hoare (`Hoare.v`):
• Hoare triples: `Assertion`, `hoare_triple`, `valid_triples`, `hoare_post_true`
• Assignment: `assn_sub`, `hoare_asgn`
• Consequence: `assert_implies`, `hoare_consequence`
• Skip: `hoare_skip`
• Sequence: `hoare_seq`
• Conditionals: `bassn`, `hoare_if`
• Loops: `hoare_while`
• Summary: complete list of Hoare Logic rules
• Assignment example, done correctly. ``` Example better_assn_example :    {{fun st => st X <= 4}}    (X ::= (APlus (AId X) (ANum 1)))    {{fun st => st X <= 5}}. Proof.    eapply hoare_consequence_pre.    apply hoare_asgn.    unfold assn_sub. simpl.    unfold t_update. simpl.    unfold assert_implies. intro st.    omega. Qed. ```
• Tutorial:
• Monday 16 October 2017 (week 5)
• Thursday 19 October 2017 (week 5)
• Lecture: Lambda calculus and Church numerals (`Church.v`):
• Untyped lambda calculus
[β] `(λx.N) M = N[x := M]`
[η] `λx.L x = L` (if `x` not free in `L`)
• Church numerals
`zero = λs. λz. z`
`one = λs. λz. s z`
`two = λs. λz. s (s z)`
`three = λs. λz. s (s (s z))`
`succ = λn. λs. λz. s (n s z)`
`plus = λm. λn. λs. λz. m s (n s z)`
`times = λm. λn. m (plus n) zero`
`plus' = λm. λn. m succ n`
`times' = λm. λn. m (plus' n) zero`
• Church booleans
`true = λt. λf. t`
`false = λt. λf. f`
`not = λb. λt. λf. b f t`
`and = λa. λb. λt. λf. a (b t f) f`
`not' = λb. b false true`
`and' = λa. λb. a b false`
`isZero = λn. n (λb. false) true`
• Church pairs
`create = λx. λy. λk. k x y`
`fst = λp. p (λx. λy. x)`
`snd = λp. p (λx. λy. y)`
• Predecessor
`pred = λn.`
`  fst (n (λp create (snd p) (succ (snd p))) (create zero zero)).`
• Fixpoint
`fix = λf. (λx. f (x x)) (λx. f (x x))`
`factorial = fix (λfact. λn. isZero n one (times n (fact (pred n))))`
• Scott numerals
`zero = λs. λz. z`
`one = λs. λz. s zero`
`two = λs. λz. s one`
`three = λs. λz. s two`
`succ = λn. λs. λz. s n`
`pred = λn. n (λp. p) zero`
`plus = fix (λplu. λm. λn. m (λp. succ (plu p n)) n)`
`times = fix (λtim. λm. λn. m (λp. plus n (tim p n)) zero)`
• Tutorial:
• Open time, catch up on whatever you wish
• Friday 20 October 2017 (week 5)
• Lecture:
• Smallstep (`Smallstep.v`):
• A Toy Language: `tm`, `eval`, `step`
• Relations: `relation`, `deterministic`
• Values: `value`
• Progress: `strong_progress`, `nf_same_as_value`
• Multi-Step Reduction (transitive closure): `multi`, `normalising`
• Equivalence of Big-Step and Small-Step Reduction: `eval_multistep`
• Small-Step Imp: `astep`, `bstep`, `cstep`
• Concurrent Imp: `CImp`
• Tutorial:
• Monday 23 October 2017 (week 6)
• Thursday 26 October 2017 (week 6)
• Lambda calculus concert!
• Friday 27 October 2017 (week 6)
• Lecture:
• Properties of Simply Typed Lambda Calculus (`StlcProp.v`):
• Progress
• Canonical forms lemma `canonical_forms_bool`, `canonical_forms_fun`
• Progress `progress`
• Preservation
• Free occurrences `appears_free_in`, `free_in_context`
• Context invariance `context_invariance`
• Substitution lemma `substitution_preserves_typing`
• Progress `preservation`
• Software Foundations in Agda
For a different approach to the same material
• Tutorial:
• As on Monday 23 October, but now fill in the proofs.
• Look also at Pairs, Empty type.
• Monday 30 October 2017 (week 7)
• Same material as Friday 27 October, this time formalised in Coq
• Review of Sum type and Empty type
• Thursday 2 November 2017 (week 7)
• Lecture: Revision. Ask me anything.
• Tutorial: Open
• Friday 3 November 2017 (week 7): no class
• Monday 6 November 2017 (week 8)
• Guest lecture: Rudi Horn. Three Approaches to Type Structure: Inference (Section 3)
• John C. Reynolds. Three approaches to type structure. In: Ehrig H., Floyd C., Nivat M., Thatcher J. (eds), Mathematical Foundations of Software Development. CAAP 1985. Lecture Notes in Computer Science, vol 185. Springer, Berlin, Heidelberg
• Thursday 9 November 2017 (week 8)
• Guest lecture: Rudi Horn. Three Approaches to Type Structure: Subtypes (Section 4)
• John C. Reynolds. Three approaches to type structure. In: Ehrig H., Floyd C., Nivat M., Thatcher J. (eds), Mathematical Foundations of Software Development. CAAP 1985. Lecture Notes in Computer Science, vol 185. Springer, Berlin, Heidelberg
• Friday 10 November 2017 (week 7): no class
• Monday 13 November 2017 (week 9)
• Guest lecture: Jakub Zalewski. Blame calculus
• Thursday 16 November 2017 (week 9)
• Friday 17 November 2017 (week 9): no class
• Monday 20 November 2017 (week 10):
• Thursday 23 November 2017 (week 10)
• Guest lecture: Rudi Horn. Three Approaches to Type Structure: Polymorphism (Section 5)
• John C. Reynolds. Three approaches to type structure. In: Ehrig H., Floyd C., Nivat M., Thatcher J. (eds), Mathematical Foundations of Software Development. CAAP 1985. Lecture Notes in Computer Science, vol 185. Springer, Berlin, Heidelberg
• Friday 24 November 2017 (week 10): no class
• Monday 27 November 2017 (week 11):
• Thursday 30 November 2017 (week 12)
• Second mock exam, taken in exam conditions
• Friday 1 December 2017 (week 12): no class

## Past papers

Go here and click on the link for past papers "Exam papers for academic sessions 2004/05 - 2016/17". Then search for "Types and Semantics".

To attempt a past paper, use Exam.v and Maps.v from Assignment 5.

## Exam

### AT-5.08 South Lab on Thursday 14 December 09:30-11:30

The final examination is worth 75% of your mark.

Because you will be working with Coq throughout the course, you should also have access to Coq for the exam. Unlike most courses with a written exam, TSPL has an online exam where you use the Coq proof assistant to assist and confirm your exam work. If anyone has any questions or concerns, please contact the instructor.

The final exam for TSPL is in December 2017

 Informatics Forum, 10 Crichton Street, Edinburgh, EH8 9AB, Scotland, UK Tel: +44 131 651 5661, Fax: +44 131 651 1426, E-mail: school-office@inf.ed.ac.uk Please contact our webadmin with any comments or corrections. Logging and Cookies Unless explicitly stated otherwise, all material is copyright © The University of Edinburgh