Aims

This module aims to bring students up to date with current research in the denotational approach to the semantics of programming languages and mathematical models of type theories, with the objective of training students to start research in theoretical computer science on these areas and their applications.

Syllabus

• Computational metalanguages
• Models of linear logic
• Universal algebra and equational logic
• Algebraic theory of effects
• Second-order algebraic theories
• Untyped lambda-calculus and recursive domain equations
• Simply-typed lambda-calculus and logical relations
• Continuations and control effects
• Dependent type theories

Objectives

On completion of this module, students should:

• be able to start research in theoretical computer science on mathematical foundations of programming languages and type theory, and their applications.

Coursework

None. This course is optional and is not for credit.

Practical work

None.

Assessment

None.

Recommended reading

Computational metalanguages

* Moggi. Computational lambda-calculus and monads. LICS 1989 pp. 14-23, IEEE Computer Society.

* Moggi. Notions of computation and monads. Information and Computation
Vol. 93 (1), Elsevier 1991, pp. 55-92.

* Plotkin and Power. Algebraic operations and generic effects. Applied
Categorical Structures 11(1), pp. 69-94, Springer 2003.

Universal algebra and equational logic

* Crole. Categories for Types (Chapter 3), pp. 120-153, Cambridge University
Press 1993.

* Baader and Nipkow. Term Rewriting and All That (Chapter 3), pp. 34-57,
Cambridge University Press 1998.

Algebraic theory of effects

* Plotkin and Power. Notions of computation determine monads, FoSSaCS, LNCS
Vol. 2303, pp. 342-356, Springer 2002.

* Hyland, Plotkin and Power. Combining effects: Sum and tensor, TCS Vol.
357(1-3), pp. 70-99, Elsevier 2006.

Second-order algebraic theories

* Fiore, Plotkin and Turi. Abstract syntax and variable binding, LICS'99,
pp. 193-203, IEEE 1999.

* Fiore and Hur. Second-order equational logic, CSL'10, pp. 320-335, ACM
2010.

* Staton. Instances of computational effects: An algebraic perspective,
LICS'13, pp. 519-528, IEEE 2013.

Untyped lambda-calculus and recursive domain equations

* Scott. Relating theories of the lambda-calculus, To H.B. Curry: essays on
combinatory logic, lambda calculus and formalism, pp. 403-450, Academic Press
1980.

* Smyth and Plotkin. The category-theoretic solution of recursive domain
equations, SIAM J. Comput. 11(4), pp. 761-783, Society for Industrial and
Applied Mathematics 1979.

Simply-typed lambda-calculus and logical relations

* Crole. Categories for Types (Chapter 4), pp. 154-200, Cambridge University
Press 1993.

* Jung and Tiuryn. A new characterization of lambda definability, TLCA, LNCS
Vol. 664, pp. 245-257, Springer 1993.

* Fiore. Semantic analysis of normalisation by evaluation for typed lambda
calculus, PPDP'02, pp. 26-37, ACM 2002.

Continuations and control effects

* Streicher and Reus. Classical logic: Continuation semantics and abstract
machines, JFP Vol. 8(6), pp.543-572, Cambridge University Press 1998.

* Thielecke. Categorical structure of continuation passing style, PhD
thesis, University of Edinburgh 1997.

* Selinger. Control categories and duality, MSCS Vol. 11(2), pp. 207-260,
Cambridge Journals 2001.

Course supplementary reading

Computational metalanguages

* Moegelberg and Staton. Linear usage of state, LMCS Vol. 10(1),
arXiv:1403.1477 2014.

* Egger, Moegelberg and Simpson. The enriched effect calculus: Syntax and
semantics, Linearity in Computation, J. Log. Comp. Vol. 24(3), pp. 615-654,
Oxford Journals 2011.

* Levy. Call-by-push-value: A subsuming paradigm, Sem. Struct. Comp. Vol. 2,
Springer 2003.

* Filinski. Monads in action, POPL'10, pp. 483-494, ACM 2010.

Universal algebra and equational logic

* Burris and Sankappanavar. A course in universal algebra, Graduate Texts in
Mathematics, 1981, Springer 1981.

* Wraith. Algebraic theories, Technical report No. 22, Aarhus University
1970. (Available on-line from Ohad Kammar's web-page.)

* Adamek, Rosicky and Vitale. Algebraic theories, Cambridge Tracts in
Mathematics Vol. 184, Cambridge University Press 2011.

* Fiore. Rough notes on algebraic theories and equational logics, MFPS'24,
2008. (Available on-line from Marcelo Fiore's web-page.)

Algebraic theory of effects

* Mellies. Segal condition meets computational effects, LICS'10, pp.
150-159, IEEE 2010.

* Plotkin and Pretnar. A logic for algebraic effects, LICS'08, pp .118-129,
IEEE 2008.

* Plotkin and Power. Adequacy for algebraic effects, FoSSaCS, LNCS Vol.
2030, pp. 1-24, Springer 2001.

* Katsumata. Relating computational effects by TT-lifting, Inf. Comp. Vol.
222, pp. 228-246, Elsevier 2013.

Second-order algebraic theories

* Fiore. Second-order and dependently-sorted abstract syntax, LICS'08, pp.
57-68, IEEE 2008.

* Fiore and Mahmoud. Second-order algebraic theories, MFCS, LNCS Vol. 6281,
pp. 368-380, Springer 2010.

* Staton. An algebraic presentation of predicate logic, FoSSaCS, LNCS Vol.
7794, pp.401-417, Springer 2013.

Untyped lambda-calculus

* Hindley and Seldin. Lambda-calculus and combinators, Cambridge University
Press 2008.

* Krivine. Lambda-calculus: types and models, Ellis Horwood 1993.

Simply-typed lambda-calculus

* Aczel. Notes on the simply typed lambda calculus, Comp. Log., NATO ASI
Series Vol. 165, pp. 57-97, Springer 1999.

* Selinger. Lecture notes on the lambda calculus, arXiv:0804.3434 2013.

Continuations and control effects

* Strachey and Wadsworth. Continuations: A mathematical Semantics for
handling full jumps, Higher-Order and Symbolic Computation Vol. 13(1-2), pp.
145-152, Springer 2000.

* Fiore and Staton. Substitution, jumps, and algebraic effects, CSL-LICS'14,
IEEE 2014. (Available on-line from Marcelo Fiore's web-page.)