3 ms·
Faux Type Theory: three minimalist OCaml simple proof checker implementations
- matt_d 1y agoAnnouncement: https://mathstodon.xyz/@andrejbauer/115191725004191889 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 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.