Computer Laboratory

Course pages 2014–15

Advanced Topics in Denotational Semantics

Principal lecturers: Prof Marcelo Fiore, Dr Ohad Kammar
Taken by: MPhil ACS, Part III
Code: L29
Hours: 16
Prerequisites: L108 Category Theory and Logic; knowledge of the material in the CST Part II Denotational Semantics and Types courses recommended.

Aims

This module aims to bring students up to date with current research in the denotational approach to the semantics of programming languages, with the objective of training students to start research in theoretical computer science on the mathematical foundations of programming languages and its applications.

Syllabus

  • Computational metalanguages [1 lecture]
  • Universal algebra and equational logic [2 lectures]
  • Algebraic theory of effects [2 lectures]
  • Effect handlers [2 lectures]
  • Effect-system semantics [1 lecture]
  • Second-order algebraic theories [2 lectures]
  • Untyped lambda-calculus and recursive domain equations [2 lectures]
  • Simply-typed lambda-calculus and logical relations [2 lecture]
  • Continuations and control effects [2 lectures]

Objectives

On completion of this module, students should:

  • be able to start research in theoretical computer science on mathematical foundations of programming languages and its applications.

Coursework

Essays

Practical work

None, but the course will include material for self-evaluation.

Assessment

The course will be assessed by means of an essay on one or more research papers related to the syllabus. Papers will be chosen by students on their own or from a given list of papers in accordance with the lecturers. The essays will be marked by the lecturers and returned to the students. Subsequently, a technical discussion with each student on the material of their essay will take place. The mark for the course will be that of the essay, with an upgrade for those students that give evidence of mastering the subject during the discussion.

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.

Effect handlers

* Plotkin and Pretnar. Handling algebraic effects, LMCS Vol. 9(4:23), pp.
1-36, arXiv:1312.1399 2013.

* Pretnar and Bauer. Programming with algebraic effects and handlers. Jour.
Log. Alg. Meth. Prog. In Press, Elsevier.

* Kammar, Lindley and Oury. Handlers in action, ICFP'13, pp. 145-158, ACM
2013.

Effect system semantics

* Wadler and Thiemann. The marriage of monads and effects, TOCL Vol. 4(1),
pp. 1-32, ACM 2003.

* Kammar and Plotkin. Algebraic foundations for type-and-effect systems,
POPL'12, pp. 349-360, ACM 2012.

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.

Effect handlers

* Kiselyov, Sabry and Swords. Extensible effects: An alternative to monad
transformers, Haskell Symposium, pp. 59-70, ACM 2013.

* Brady. Programming and reasoning with algebraic effects and dependent
types, ICFP'13, pp. 133-144, ACM 2013.

* Pretnar and Bauer. An effect system for algebraic effects and handlers,
Algebra and Coalgebra in Computer Science, LNCS Vol. 8089, pp. 1-16, Springer
2013.

Effect system semantics

* Lucassen and Gifford. Polymorphic effect systems, POPL'88, pp. 47-57, ACM
1988.

* Benton, Kennedy, Hofmann and Beringer. Reading, writing, and relations:
Towards extensional semantics for effect analysis, Prog. Lang. Sys., LNCS
Vol. 4279, pp. 114-130, Springer 2006.

* Katsumata. Parametric effect monads and semantics of effect systems,
POPL'14, pp. 633-645, ACM 2014.

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.

Local effects

* Stark. Free algebra models for the pi-calculus, FoSSaCS, LNCS Vol. 3441,
pp. 155-169, Springer 2005.

* Levy. Possible world semantics for general storage in call-by-value, CSL,
LNCS Vol. 2471, pp. 232-246, Springer 2002.

* Mellies. Local states in string diagrams, RTLC, LNCS 8560, pp. 334-348,
Springer 2014.

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.)