Structural logical relations with case analysis and equality reasoning

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

Standard

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

Harvard

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

APA

Rasmussen, U. T., & 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 (pp. 43-54). Association for Computing Machinery. https://doi.org/10.1145/2503887.2503891

Vancouver

Rasmussen UT, Filinski A. 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. 2013. p. 43-54 https://doi.org/10.1145/2503887.2503891

Author

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

Bibtex

@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",

}

RIS

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 -

ID: 101201784