CADE Tutorial/Next

If you want to read more about STELF, you can check out the introductions, tutorials, and case studies on the wiki.

We strongly recommend that you work on some of the following exercises: you’ll get a flavor for the experience of defining systems and proving theorems in STELF. If we have time at the end of the tutorial, we’ll break into small groups and you can pick an interesting problem or two to work on. If you get stuck, ask a TA! Refer to the solutions to check your work (though Server OK from STELF should be assurance enough!) Feel free to ask us for help during the rest of the conference.

Beginner problems (Recommended)

• Preservation for MinML — Prove type preservation for MinML. (Solution)
• Sequent calculus vs. natural deduction — Prove the logical equivalence of Gentzen’s intuitionistic sequent calculus and intuitionistic natural deduction. (Solution)
• Big-step evaluation vs. small-step transition semantics — Prove the operational equivalence of the big-step and small-step views of operational semantics. (Solution)

Intermediate problems

• Call-by-value CPS transform, with administrative redexes — Define an algorithm for converting lambda terms to continuation-passing style (Solution)
• Higher-order call-by-value CPS transform, no administrative redexes — Define a higher-order variant of the CPS conversion that never creates administrative redexes (Solution)
• Church-Rosser — Prove Church and Rosser’s seminal result via a Diamond Lemma for the untyped lambda calculus. (Solution)
• MinML with exceptions — Prove type safety for an extension of MinML with exceptions defined using structural operational semantics with a “raises” judgement. (Solution)
• Lambda calculus and combinators — Explore the relation between the simply-typed lambda calculus and combinatory logic using Curry’s classic bracket abstraction algorithm. (Solution)