POPL Tutorial/Session 5

In this session, you’ll get a flavor for the experience of defining systems and proving theorems in STELF. Break into small groups and 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!)

_Please fill [https://spreadsheets.google.com/viewform?key=p0-89EvFXQhUXF827jjk_Dg feedback form]_

Beginner problems (Recommended)

• 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)
• Lambda calculus and combinators — Explore the relation between the simply-typed lambda calculus and combinatory logic using Curry’s classic bracket abstraction algorithm. (Solution)
• Church-Rosser — Prove Church and Rosser’s seminal result via a Diamond Lemma for the untyped lambda calculus. (Solution)

Advanced problems

• MinML with exceptions — Prove type safety for an extension of MinML with exceptions defined using structural operational semantics with a “raises” judgement. (Solution)