Formalization of Proofs by Logical Relations in a Logical Framework

Ulrik Rasmussen
September, 2013
Master's Thesis


Logical relations are an important proof technique frequently employed in the study of programming languages based on typed lambda calculi, where they have been used to prove a broad range of foundational properties. We present applications and extensions of the method of structural logical relations by Schürmann and Sarnat [In Proc. of 23rd Symp. on Logic in Computer Science, 2008], which enables syntactic and verifiable representations of proofs by logical relations in the Twelf proof assistant by reducing problems to a consistency proof of an auxiliary logic. We apply the method in several case studies where we formalize logical relations for prototypical programming languages. We identify shortcomings of the existing method, which we address by extending the auxiliary logic with several new reasoning principles.