User guide for Cubint

Christian Müller

Abstract:

The simply typed $\lambda$-calculus (S), system F, F$\omega$ 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.