The simply typed -calculus (S), system F, F and the calculus of construction (CC) offer a good framework to understand the underlying theory of programming languages. Cubint is an interpreter for these calculi that lets you play around with examples to deepen your understanding. This document should provide all the things that you need to know in order to work with the interpreter.

The first section crash course is intended for the audience of the semantics lecture at the computer science department of UdS. It offers introductory material that enables students to use the interpreter in the first few weeks of the lecture.

- Crash Course

- Getting Cubint
- rlwrap or emacs
- Commands
- Expressions
- S - Simply Typed -Calculus
- F - System F
- Fw - F
- CC - Calculus of Construction
- R - Type Reconstruction for Prenex Polymorphism
- RG - Type Reconstruction Based on Graphs
- U - Untyped Lambda Cube
- UD - User Defined
- SUB - Subtyping

- Stepwise Reduction
- Further Readings
- About this document ...

Christian Müller 2004-11-09