Faux Type Theory: three minimalist OCaml simple proof checker implementations

https://github.com/andrejbauer/faux-type-theory

by matt_d • 10 months ago

3 1 10 months ago

matt_d• 10 months ago

Announcement:

https://mathstodon.xyz/@andrejbauer/115191725004191889

This week I gave a lecture series at the School on Logical Frameworks and Proof Systems Interoperability. I spoke about programming language techniques for proof assistants. The lecture slides and the reference implementations of a minimalist type theory are available at:

https://github.com/andrejbauer/faux-type-theory

The repository has three minimalist OCaml implementations of a simple proof checker:
1. A basic one showing how to implement bidirectional type checking and type-directed equality checking, using monadic style programming.
2. An extension with rudimentary holes (meta-variables) and unification.
3. A version that implements "variables as computational effects", using native OCaml 5 effects and handlers.

Faux Type Theory: three minimalist OCaml simple proof checker implementations

Related Stories