Semantics: Resources

Saarland University

Computer Science

Programming Systems

Lecture Notes

Coq

Coq Home Page (download system here, we are using version 8.2)
Coq Documents
Coq Tutorial by Benjamin C. Pierce

Standard ML

Programming in Standard ML, by Robert Harper, CMU.
Programmierung, by Gert Smolka, (in German)
Alice, an implementation of Standard ML with a nice GUI
Moscow ML, a lean implementation of Standard ML
The Standard ML Basis Library
Wikipedia entry for Standard ML

Comp.Lang.ML FAQ

Further Reading

Benjamin C. Pierce, Types and Programming Languages, The MIT Press, 2003.
Robert Harper, Practical Foundations for Programming Languages CMU, 2009.
Zhaohui Luo, Computation and reasoning: a type theory for Computer Science. Oxford University Press, 1994.
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.
Henk Barendregt, Lambda Calculi with Types. Handbook of Logic in Computer Science, Volume 2, 1992.
Jean-Yves Girard, Proofs and Types. Translated and with appendices by Paul Taylor and Yves Lafont, Cambridge University Press, 1990.
Glynn Winskel, The Formal Semantics of Programming Languages: An Introduction. MIT Press, 1993.
Benjamin C. Pierce (ed), Advanced Topics in Types and Programming Languages, The MIT Press, 2005.
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 tutorial introduction to Barendrengt's lambda cube and pure type systems:
- Simon Peyton Jones and Erik Meijer, Henk: a typed intermediate language, 1997.

Last Change: Thu Apr 25 20:17:38 2013 |