Structural Logical Relations

Carsten Schürmann, Jeffrey Sarnat

Research output: Journal Article or Conference Article in JournalConference articleResearchpeer-review

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.
Original languageEnglish
JournalLogic in Computer Science
Pages (from-to)69-82
ISSN1043-6871
Publication statusPublished - 2008
Event23rd Annual IEEE Symposium on Logic in Computer Science (LICS 2008) - Pittsburgh, Pennsylvania, United States
Duration: 24 Jun 200827 Jun 2008
Conference number: 23

Conference

Conference23rd Annual IEEE Symposium on Logic in Computer Science (LICS 2008)
Number23
Country/TerritoryUnited States
CityPittsburgh, Pennsylvania
Period24/06/200827/06/2008

Cite this