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.