# Structural Logical Relations with Case Analysis and Equality Reasoning

Ulrik Rasmussen, Andrzej Filinski

September, 2013

Proceedings International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP)

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

@inproceedings{rasmussen2013a,
author = {Ulrik Rasmussen, Andrzej Filinski},
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Ã¼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.},
year = {2013},
month = {September},
booktitle = {Proceedings International Workshop on Logical Frameworks and
Meta-Languages: Theory and Practice (LFMTP)},
doi = {10.1145/2503887.2503891},
}