A small functional language

Our language combines literals, variables, pairs, functions, application, and let bindings. Its chapters are organized in two sections, which follow its development from syntax to declarative typing rules.

The Syntax section describes the language and how its programs are read:

Parsing encodes the behavior of parsers as relations, which are then used to prove parser implementation's correctness.

Language syntax describes expressions and the token sequences that represent them.

Recursive descent implements the parser combinators and proves their correctness.

The Typechecking section explains which types expressions may have:

Basic concepts introduces types, schemes, and typing contexts.

Unification explains substitutions and what it means to make two types agree.

Algorithm W states the typing rules and the contract for inference.

The series is a work in progress. The inference contract is a specification; the executable inference procedure remains to be developed.