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 Citationer (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.

Originalsprog	Engelsk
Titel	LFMTP '13 : proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks & Meta-Languages: theory & practice
Antal sider	12
Forlag	Association for Computing Machinery
Publikationsdato	2013
Sider	43-54
ISBN (Elektronisk)	978-1-4503-2382-6
DOI	https://doi.org/10.1145/2503887.2503891
Status	Udgivet - 2013
Begivenhed	8th ACM SIGPLAN International Workshop on Logical Frameworks & Meta-Languages: theory & practice - Boston, USA Varighed: 23 sep. 2013 → 23 sep. 2013 Konferencens nummer: 8

Konference

Konference	8th ACM SIGPLAN International Workshop on Logical Frameworks & Meta-Languages
Nummer	8
Land/Område	USA
By	Boston
Periode	23/09/2013 → 23/09/2013

Adgang til dokumentet

10.1145/2503887.2503891

Citationsformater

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. s. 43-54.

Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › peer review

Rasmussen, UT & Filinski, A 2013, Structural logical relations with case analysis and equality reasoning. i LFMTP '13: proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks & Meta-Languages: theory & practice. Association for Computing Machinery, s. 43-54, 8th ACM SIGPLAN International Workshop on Logical Frameworks & Meta-Languages, Boston, USA, 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 -