Programs & Proofs: Working in Type Theory

Summerschool
14 - 18 August 1995
Hetzelsdorf, Fränkische Schweiz

This is the WWW-page of an an advanced summerschool on program development and verification in a type-theoretic environment organised by the Erlanger Dienstagsclub. The programme centered around the interactive proof assistant LEGO designed and implemented by Randy Pollack

LEGO is based on a Unifying Theory of dependent Types (UTT), which combines Luo's Extended Calculus of Constructions with Martin-Löf type theory. Type theory treats both programs and their correctness proofs as first-class citizens, supplying an expressive framework for Program Specification, Program Development and Reasoning about Programs.

LEGO and its underlying type theory was introduced and explored in lectures and laboratory sessions with exercises and experiments at the terminal. Applications of type theory comes in different flavours and the course gave a comprehensive introduction to different approaches. Exploiting the LEGO system both as an object language and a meta language, the various aspects are captured in the following central themes

• LEGO as a basis for functional programming
• LEGO as a basis for imperative programming
• LEGO as a basis for operational semantics and concurrency

• List of participants
• Programme of the summerschool
• Exercises and solutions
• The results of the exercises for each guest login produced during the summerschool.

For more detailed information please contact: info@dienstagsclub.org

Martin Steffen, Terry Stroup, Thomas Schreiber, Uwe Nestmann (August 1995)

This research was supported by the Deutsche Forschungsgemeinschaft, Sonderforschungsbereich 182, project C2, and by the Deutscher Akademischer Austauschdienst within the ARC-programme Ko-Entwicklung objektorientierter Programme in LEGO.