Saarland University
Informatics
Programming Systems
Teaching
Semantics 2007
Main page
Literature
Lecture Notes
Timetable
Registration
Services
Exams and Grade
Login
Forum
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 F-Omega 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
- A survey of object-oriented concepts, and a foundational model of object-oriented
languages, 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,
Proof-checking using Dependent Type Systems.
Handbook of Artificial Reasoning, Volume II,
Ch. 18 (2001), 1149--1240.
About pure type systems and the Curry-Howard Correspondence
for higher-order predicate logic.
- Jean-Yves 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: Thu 01 Jan 1970 00:00:00 UTC
|