Computer Laboratory

Course pages 2012–13

Categorical Models of Computational Languages

Principal lecturer: Prof Marcelo Fiore
Taken by: MPhil ACS, Part III
Code: L24
Hours: 8
Prerequisites: L108 Category Theory and Logic; knowledge of the material in the Part II `Denotational Semantics' and `Types' courses would be a bonus.

Aims

The course explores the mathematical structures used to model a wide range of computational languages. These will be considered from the following viewpoints: (i) type discipline; (ii) data structuring; (iii) calling mechanisms; (iv) programming primitives; (v) resource management; and (vi) operational semantics. Overall we will look at: (i) untyped and typed languages, and, amongst the latter, simple, polymorphic, and dependently typed; (ii) inductive and recursively defined datatypes; (iii) call-by-name, call-by-value, and mixed paradigms; (iv) computational effects and control operators; (v) linearity; and (vi) reduction vs interaction.

Syllabus

Computational Languages Categorical Structures
  • Untyped lambda-calculus
  • Simply-typed and Polymorphic lambda-calculus
  • Dependent Type Theory
  • Fixed Point Calculus (FPC).
  • Computational lambda-calculus and Call-By-Push-Value
  • Dual calculi
  • Linear Logic
  • Process calculi
  • Limits and colimits
  • Adjunctions
  • Locally cartesian closed categories
  • Algebras, coalgebras, and bialgebras
  • Monads and comonads
  • Enriched, indexed, and fibred categories
  • Symmetric monoidal closed categories
  • Distributive laws

Objectives

On completion of this module students should be able to start research in areas of theoretical computer science involving categorical modelling.

Coursework

None

Practical work

None

Assessment

The course will be assessed by means of an essay on one or more research papers related to the syllabus. Assessment will be by coursework and an oral discussion assessed by Professor Fiore.

Recommended reading

Students intending to take the course should read the following primary text before the beginning of Lent term:
Crole, R. (1993). Categories for types. Cambridge University Press

Further recommended reading:

  • Dybjer, P.(1996) Internal Type Theory. In Types'95, LNCS, 1996.
  • Egger, J. Mogelberg, R. & Simpson, A. (2009) Enriching an effect calculus with linear types. CSL'09, 2009.
  • Fiore, M. (1996) Axiomatic Domain Theory in Categories of Partial Maps. Cambridge University Press
  • Fiore, M. (2002) Semantic analysis of normalisation by evaluation for typed lambda calculus. In PPDP'02, 2002.
  • Fiore, M. Moggi, E. & Sangiorgi, D. (2002) A fully-abstract model for the pi-calculus. Information and Computation 179, 76-117, 2002.
  • Fiore, M. Plotkin, G. & Turi, D. (1999) Abstract syntax and variable binding. In LICS'99, pages 193-202, 1999.
  • Fiore, M. & Turi, D. (2001) Semantics of name and value passing. In LICS'01, pp 93-104, 2001.
  • Girard, J.-Y. (1991) A new constructive logic: classical logic. Mathematical Structures in Computer Science, pp 255-296, 1991.
  • Harmer, R., Hyland, M., & Mellies, P.-A. (2007) Categorical combinatorics for innocent strategies. In LICS'07, pp 379-388, 2007.
  • Hofmann, M. (1997) Syntax and Semantics of Dependent Types. In Semantics and Logics of Computation, pp 79-130. Cambridge University Press, 1997.
  • Hofmann, M., & Streicher, T. (1998) The groupoid interpretation of type theory. In Twenty-five years of constructive type theory, pp 83-111, 1998.
  • Jacobs, B. (2001) Categorical logic and type theory. Elsevier
  • Lambek, J. & Scott, P. (1988) Introduction to higher-order categorical logic. Cambridge Studies in Advanced Mathematics (No. 7)
  • Levy, P. (2005) Adjunction models for call-by-push-value with stacks. Theory and Applications of Categories, Vol. 14, No. 5, pp 75-110, 2005.
  • Mellies, P.-A. (2009) Categorical semantics of linear logic. In Panoramas et Syntheses 27, 2009.
  • Moggi, E. (1991) Notions of computation and monads. Information and Computation, 93(1):55-92, 1991.
  • Plotkin, G., & A.J. Power. (2002) Notions of computation determine monads. In FOSSACS'02, LNCS 2303, pp 342-356, 2002.
  • Scott, D. (1980) Relating theories of the lambda-calculus. In To H.B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalisms. Academic Press, 1980.
  • Seely, R.A.G. (1984) Locally cartesian closed categories and type theory. Proceedings of the Cambridge Philosophical Society, 95:33-4, 1984.
  • Selinger, P. (2001) Control Categories and Duality: on the Categorical Semantics of the Lambda-Mu Calculus. Math. Struct. in Comp. Science, vol. 11, pp 207-260, 2001.
  • Smyth, M. & Plotkin, G. (1982) The category-theoretic solution of recursive domain equations. SIAM Journal of Computing 11:761-783, 1982.
  • Streicher, T. & Reus, B. (1998) Classical logic: Continuation Semantics and Abstract Machines. Journal of Functional Programming, Vol 8(6), pp 543-572, 1998.
  • Turi, D. & Plotkin, G. (1997) Towards a mathematical operational semantics. In LICS'97, pp 280-291, 1997.
  • Wadler, P. (2003) Call-by-value is dual to call-by-name. In ICFP'03, 2003.
  • Wadler, P. (2005) Call-by-value is dual to call-by-name, reloaded. In RTA'05, 2005.