Structural logical relations with case analysis and equality reasoning

Ulrik Terp Rasmussen; Andrzej Filinski

doi:10.1145/2503887.2503891

Structural logical relations with case analysis and equality reasoning

3 Citations (Scopus)

Abstract

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 language	English
Title of host publication	LFMTP '13 : proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks & Meta-Languages: theory & practice
Number of pages	12
Publisher	Association for Computing Machinery
Publication date	2013
Pages	43-54
ISBN (Electronic)	978-1-4503-2382-6
DOIs	https://doi.org/10.1145/2503887.2503891
Publication status	Published - 2013
Event	8th ACM SIGPLAN International Workshop on Logical Frameworks & Meta-Languages: theory & practice - Boston, United States Duration: 23 Sept 2013 → 23 Sept 2013 Conference number: 8

Conference

Conference	8th ACM SIGPLAN International Workshop on Logical Frameworks & Meta-Languages
Number	8
Country/Territory	United States
City	Boston
Period	23/09/2013 → 23/09/2013

Access to Document

10.1145/2503887.2503891

Cite this

Structural logical relations with case analysis and equality reasoning. / Rasmussen, Ulrik Terp; Filinski, Andrzej.
LFMTP '13: proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks & Meta-Languages: theory & practice. Association for Computing Machinery, 2013. p. 43-54.

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

Rasmussen, UT & Filinski, A 2013, Structural logical relations with case analysis and equality reasoning. in LFMTP '13: proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks & Meta-Languages: theory & practice. Association for Computing Machinery, pp. 43-54, 8th ACM SIGPLAN International Workshop on Logical Frameworks & Meta-Languages, Boston, United States, 23/09/2013. https://doi.org/10.1145/2503887.2503891

@inproceedings{39682cb27a58468db882462e9c83809c,

title = "Structural logical relations with case analysis and equality reasoning",

abstract = "Formalizing proofs by logical relations in the Twelf proof assistant is known to be notoriously difficult. However, as demonstrated by Sch{\"u}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.",

author = "Rasmussen, {Ulrik Terp} and Andrzej Filinski",

year = "2013",

doi = "10.1145/2503887.2503891",

language = "English",

pages = "43--54",

booktitle = "LFMTP '13",

publisher = "Association for Computing Machinery",

note = "8th ACM SIGPLAN International Workshop on Logical Frameworks & Meta-Languages : theory & practice, LFMTP '13 ; Conference date: 23-09-2013 Through 23-09-2013",

}

TY - GEN

T1 - Structural logical relations with case analysis and equality reasoning

AU - Rasmussen, Ulrik Terp

AU - Filinski, Andrzej

N1 - Conference code: 8

PY - 2013

Y1 - 2013

N2 - 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.

AB - 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.

U2 - 10.1145/2503887.2503891

DO - 10.1145/2503887.2503891

M3 - Article in proceedings

SP - 43

EP - 54

BT - LFMTP '13

PB - Association for Computing Machinery

T2 - 8th ACM SIGPLAN International Workshop on Logical Frameworks & Meta-Languages

Y2 - 23 September 2013 through 23 September 2013

ER -