I've attached a Twelf file containing a definition of a simply-typed lambda calculus with just booleans as a ground type and a proof of preservation and progress. This is roughly the content of chapter 8.
I've also attached a somewhat-less-relevant Twelf development defining translations from the untyped lambda calculus to the SKI combinator calculus and vice versa, with proofs that these translations are simulation relations. Warning: impenetrable variable names.
Ben showed me the twelf site, and some sample code on his laptop.
The idea is to use twelf language to implement ideas from the "Practical Foundations" book.
![[paper clip]](/cours/static/images/paper_clip_tilt.png)
