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
  • Benjamin C. Pierce, Types and Programming Languages, The MIT Press, 2003.


• Similar courses exist at
  • CMU: Type Systems
  • UPenn: Software Foundations
  • Chigago: Advanced Type Systems


• We use the programming language Standard ML. Some useful links:
  • Programming in Standard ML, by Robert Harper, CMU.
  • Programmierung, by Gert Smolka, an introduction to programming using Standard ML (in German)
  • Alice, an implementation of Standard ML with a very nice GUI
  • Moscow ML, a lean implementation of Standard ML
  • The Standard ML Basis Library
  • Wikipedia entry for Standard ML
  • Comp.Lang.ML FAQ


• 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:
  • Simon Peyton Jones and Erik Meijer, Henk: a typed intermediate language, 1997.


• The basic definitions and results concerning confluence and termination can be found in
  • Franz Baader and Tobias Nipkow, Term Rewriting and All That. Cambridge University Press, 1998.


• A survey of object-oriented concepts, and a foundational model of object-oriented languages, can be found in
  • Martín Abadi and Luca Cardelli, A Theory of Objects. Springer, 1996.


• 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.