Universität des Saarlandes
FR Informatik
Programmiersysteme
Vorlesungen
Semantics WS 03


Homepage
Literature
Timetable
Registration
Tutorials
Exams
Mailing List

Semantics: Literature

• The lecture will be based on the book
  Benjamin C. Pierce, Types and Programming Languages, The MIT Press, 2003. (Table of contents)

• A course at UPenn based on the book: CIS 500: Software Foundations

• Here are the lecture notes on minimization.

• Simon Peyton Jones and Erik Meijer, Henk: a typed intermediate language. 1997.

  This paper gives a tutorial introduction to the lambda cube.

• Henk Barendregt and Herman Geuvers, Proof-checking using Dependent Type Systems. Handbook of Artificial Reasoning, Volume II, Ch. 18 (2001), 1149--1240.

  The lambda cube can be generalized to pure type systems. If you want to know more about about the lambda cube, pure type systems and the Curry-Howard Correspondence for higher-order predicate logic, this is the right place to start. Great stuff!

Last change: Thu 01 Jan 1970 00:00:00 UTC