Formalization of Proofs by Logical Relations in a Logical Framework

Abstract

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.

@mastersthesis{rasmussen2013,
  author = {Ulrik Rasmussen},
  title = {Formalization of Proofs by Logical Relations in a Logical Framework},
  abstract = {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\"{u}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. },
  year = {2013},
  month = {September},
  note = {Master's Thesis},
  school = {University of Copenhagen},
}