Structural logical relations with case analysis and equality reasoning

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

Formalizing proofs by logical relations in the Twelf proof assistant is known to be notoriously difficult. However, as demonstrated by Schürmann and Sarnat [In Proc. of 23rd Symp. on Logic in Computer Science, 2008] such proofs can be represented and verified in Twelf if done so using a Gentzen-style auxiliary assertion logic which is subsequently proved consistent via cut elimination.

We demonstrate in this paper an application of the above methodology to proofs of observational equivalence between expressions in a simply typed lambda calculus with a call-by-name operational semantics. Our use case requires the assertion logic to be extended with reasoning principles not present in the original presentation of the formalization method. We address this by generalizing the assertion logic to include dependent sorts, and demonstrate that the original cut elimination proof continues to apply without modification.
Original languageEnglish
Title of host publicationLFMTP '13 : proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks & Meta-Languages: theory & practice
Number of pages12
PublisherAssociation for Computing Machinery
Publication date2013
Pages43-54
ISBN (Electronic)978-1-4503-2382-6
DOIs
Publication statusPublished - 2013
Event8th ACM SIGPLAN International Workshop on Logical Frameworks & Meta-Languages: theory & practice - Boston, United States
Duration: 23 Sep 201323 Sep 2013
Conference number: 8

Conference

Conference8th ACM SIGPLAN International Workshop on Logical Frameworks & Meta-Languages
Nummer8
LandUnited States
ByBoston
Periode23/09/201323/09/2013

ID: 101201784