Saarland University
Computer Science
Programming Systems
Teaching
Semantics WS 05
Main
Literature
Timetable
Registration
Services
Exams
Semantics: Literature

Much of the course is based on the book

Similar courses exist at
 We use the programming language Standard ML.
Some useful links:
 We implement F and FOmega using uniform syntax. This
approach is based on Barendrengt's lambda cube and
pure type systems. A tutorial introduction:
 The basic definitions and results concerning confluence and termination
can be found in
 Advanced literature:
 Henk Barendregt,
Lambda Calculi with Types.
Handbook of Logic in Computer Science, Volume 2, 1992.
 Henk Barendregt and Herman Geuvers,
Proofchecking using Dependent Type Systems.
Handbook of Artificial Reasoning, Volume II,
Ch. 18 (2001), 11491240.
About pure type systems and the CurryHoward Correspondence
for higherorder predicate logic.
 JeanYves Girard,
Proofs and Types.
Translated and with appendices by
Paul Taylor and Yves Lafont,
Cambridge University Press, 1990.

Benjamin C. Pierce (ed),
Advanced Topics in Types and Programming Languages,
The MIT Press, 2005.
Last Change: Sat Oct 28 17:12:37 2017