Structural Logical Relations

 



 
 

People

  • Jeffrey Sarnat
  • Carsten Schürmann

Abstract

Tait's method (a.k.a. proof by logical relations) is a powerful proof technique frequently used for showing foundational properties of languages based on typed \lambda-calculi. Historically, these proofs have been extremely difficult to formalize in proof assistants with weak meta-logics, such as Twelf, and yet they are often straightforward in proof assistants with stronger meta-logics. In this paper, we propose structural logical relations as a technique for conducting these proofs in systems with limited meta-logical strength by explicitly representing and reasoning about an auxiliary logic. In support of our claims, we give a Twelf-checked proof of the completeness of an algorithm for checking equality of simply typed lambda-terms.

Source Code

Weak normalization of the simply-typed lambda-calculus.
Decidability of equivalence checking.
Weak normalization of System F. This version only works with the latest version of Twelf in the Twelf repository. Since the proof theoretic strength of second order logic exceeds the proof theoretic strength of the meta-logic of Twelf, the cut-elimination procedure for second order does not termination check. Please selection Twelf.unsafe from the options menu. Thank you. (If you have questions about the how and why, send mail to carsten@itu.dk).
Weak normalization of the monadic lambda-calculus

Papers

Structural Logical Relations. To appear at LICS'08.
Technical Report. Under revision.