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) callbyname, callbyvalue, and mixed paradigms; (iv) computational effects and control operators; (v) linearity; and (vi) reduction vs interaction.
Syllabus
Computational Languages  Categorical Structures 



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 fullyabstract model for the picalculus. Information and Computation 179, 76117, 2002.
 Fiore, M. Plotkin, G. & Turi, D. (1999) Abstract syntax and variable binding. In LICS'99, pages 193202, 1999.
 Fiore, M. & Turi, D. (2001) Semantics of name and value passing. In LICS'01, pp 93104, 2001.
 Girard, J.Y. (1991) A new constructive logic: classical logic. Mathematical Structures in Computer Science, pp 255296, 1991.
 Harmer, R., Hyland, M., & Mellies, P.A. (2007) Categorical combinatorics for innocent strategies. In LICS'07, pp 379388, 2007.
 Hofmann, M. (1997) Syntax and Semantics of Dependent Types. In Semantics and Logics of Computation, pp 79130. Cambridge University Press, 1997.
 Hofmann, M., & Streicher, T. (1998) The groupoid interpretation of type theory. In Twentyfive years of constructive type theory, pp 83111, 1998.
 Jacobs, B. (2001) Categorical logic and type theory. Elsevier
 Lambek, J. & Scott, P. (1988) Introduction to higherorder categorical logic. Cambridge Studies in Advanced Mathematics (No. 7)
 Levy, P. (2005) Adjunction models for callbypushvalue with stacks. Theory and Applications of Categories, Vol. 14, No. 5, pp 75110, 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):5592, 1991.
 Plotkin, G., & A.J. Power. (2002) Notions of computation determine monads. In FOSSACS'02, LNCS 2303, pp 342356, 2002.
 Scott, D. (1980) Relating theories of the lambdacalculus. 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:334, 1984.
 Selinger, P. (2001) Control Categories and Duality: on the Categorical Semantics of the LambdaMu Calculus. Math. Struct. in Comp. Science, vol. 11, pp 207260, 2001.
 Smyth, M. & Plotkin, G. (1982) The categorytheoretic solution of recursive domain equations. SIAM Journal of Computing 11:761783, 1982.
 Streicher, T. & Reus, B. (1998) Classical logic: Continuation Semantics and Abstract Machines. Journal of Functional Programming, Vol 8(6), pp 543572, 1998.
 Turi, D. & Plotkin, G. (1997) Towards a mathematical operational semantics. In LICS'97, pp 280291, 1997.
 Wadler, P. (2003) Callbyvalue is dual to callbyname. In ICFP'03, 2003.
 Wadler, P. (2005) Callbyvalue is dual to callbyname, reloaded. In RTA'05, 2005.