Viktor Vafeiadis

Semantics of Programming Languages

First Supervision

1. Explain the term 'semantics'. Which three types of semantics are useful for programming languages.
2. Why are type systems useful? Give an example of a program in L1 that fails. Prove that it is not typeable.
3. (a) What is meant by progress, type preservation and safety.
   (b) Consider a language L0 containing only boolean and integer constants, integer addition, and if expressions. Give the form of the typing jugdment and the reduction relation for terms in L0. Give full typing rules and small-step operational semantics for L0. Is L0's type-checking decidable? What about typeability?
   (c) Show that the expression if true then 1 + 2 else 4 is well typed. Show its evaluation.
   (d) State and prove a safety theorem for your language.
   
4. Do exercises 1, 2, 8, 10 from page 39 of the lecture notes.

Second Supervision

1. Define terms in simply-typed lambda-calculus (i.e. expressions consisting of variables, integer constants, functions abstractions, function applications, but no operations on store). Write down typing rules.
2. Explain alpha-conversion, de Bruijn indices and substitution.
3. Explain the difference between call by value, call-by-name, and call by need. Give operational semantics for call by value and call by name. How can we model call by need?
4. State progress, type preservation and safety theorems for lamda-calculus.
5. Briefly explain how we can extend our language to support features such as: recursion, mutual recursion, tuples, records, ML datatypes, and lists.

Third Supervision

1. Explain the terms covariance, contravariance and invariance with respect to sub-typing. Give an example for each.
2. year 2003 paper 6 question 12 (subtyping)
   year 2004 paper 6 question 11 (semantic equivalence)
   year 2003 paper 5 question 11 (L2)
   year 2004 paper 5 question 11 (L2)
   

Return to main page...