> 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:
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.