Saarland University
Computer Science
Programming Systems
Teaching
Advanced Topics in Semantics


Main page
Literature
Programme
Discussion board

Advanced Topics in Semantics: Literature

Basic reading

• Benjamin Pierce, Types and Programming Languages, MIT Press, 2002.
• Benjamin Pierce (ed.), Advanced Topics in Types and Programming Languages, MIT Press, 2005.

Further reading

• Phil Wadler, A Taste of Linear Logic, Proc. Mathematical Foundations of Computer Science, LNCS vol 711, pp. 185-210, 1993.
• Harry Mairson, A simple proof of a theorem of Statman, Theoretical Computer Science 103 (1992), pp. 387-394.
• Some links to further literature on type theory for modules.

On presentations

• How to present a paper in theoretical computer science, by Ian Parberry.

Possible topics for presentations

Substructural type systems and resources, effect type systems

• On bunched typing by Peter O'Hearn, Journal of Functional Programming, 13(4):747-796, 2003.
• Effect types and region-based memory management by Fritz Henglein et al., Chap. 3 of ATTPL.
• Reading, writing and relations: towards extensional semantics for effect analyses by Nick Benton et el., Proc. APLAS'06, Springer LNCS vol 4279.
• A type system for bounded space and functional in-place update or "how to compile functional programs into malloc()-free C" by Martin Hofmann, Nordic Journal of Computing 7(4):258-289, 2000.

Models of types, logical relations, and reasoning about programs

• An indexed model of recursive types for foundational proof-carrying code by Andrew Appel and David McAllester, ACM Toplas, 23(5):657-683, 2001.
• Semantic types: a fresh look at the ideal models for types by Jérôme Vouillon and Paul-André Melliès, Proc. POPL'04.
• Kripke-style models for typed lambda calculus by John Mitchell and Eugenio Moggi, Journal Of Pure And Applied Algebra, 51, 1991.
• Typed operational reasoning by Andrew Pitts, Chap. 7 of ATTPL.
• Operational reasoning for functions with local state by Andrew Pitts and Ian Stark, pp. 227-273 in Higher-order Operational Techniques in Semantics, Cambridge University Press, 1998.

Type dependency and module systems

• Dependent types by David Aspinall and Martin Hofmann, Chap. 2 of ATTPL.
• Type definitions by Christopher Stone, Chap. 9 of ATTPL.

Types and logics for low-level languages

• Proof-carrying code by George Necula, Chap. 5 of ATTPL.
• A typed compositional logic for a stack-based abstract machine by Nick Benton, Proc. APLAS'05, Springer LNCS vol 3780.