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
APA
Vancouver
Author
Bibtex
}
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