Examples

The following examples are distributed with Adelfa:

First Order

• Properties of Lists
• Every natural number is either even or odd
• Existence of an identity element for addition
• Less than or equal to is monotonic over addition
• Map distributes over append

$\lambda$-Calculus

• Subject Reduction for the simply typed $\lambda$-calculus
• Uniqueness of typing for the simply typed $\lambda$-calculus

Logic

• Admissibility of cut for simple intuitionistic sequent calculus

Programming Languages

• A solution to problem 1a of the POPLMark challenge