Examples

Palindromes

Inductively-defined predicates are used to specify palindromes. This specification is used to prove the correctness of a function that checks whether a list is, in fact, a palindrome.

Binary Search Trees

A verified implementation of binary search trees.

A Certified Type Checker

A specification of a simple type system together with a type checker that's proven correct.

The Well-Typed Interpreter

Dependent types are used to rule out run-time errors for a small interpreter.

Dependent de Bruijn Indices

In a simply-typed lambda-calculus, variables are encoded as intrinsically-typed references into a context, capturing both the number of intervening binders and the corresponding type. This representation is then used as the basis for a constant folding pass, which is proved correct.

Parametric Higher-Order Abstract Syntax (PHOAS)

Intrinsically-typed terms are represented in the PHOAS style, which is a higher-order encoding that's suitable for interactive theorem provers based on full dependent types. This is used to implement constant folding and prove it correct.

Metaprogramming: Balanced Parentheses

A demonstration of Lean's syntax extension capabilities in which new syntax rules are added that match parentheses and braces.

Metaprogramming: Arithmetic Expressions

A more involved example of syntax extension that demonstrates the use of precedence and associativity.