Course pages 2015–16

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