TY - JOUR
T1 - Logical relations for a logical framework
AU - Rabe, Florian
AU - Sojakova, Kristina
PY - 2013/11
Y1 - 2013/11
N2 - Logical relations are a central concept used to study various higher-order type theories and occur frequently in the proofs of a wide variety of meta-theorems. Besides extending the logical relation principle to more general languages, an important research question has been how to represent and thus verify logical relation arguments in logical frameworks. We formulate a theory of logical relations for Dependent Type Theory (DTT) with β η-equality which guarantees that any valid logical relation satisfies the Basic Lemma. Our definition is syntactic and reflective in the sense that a relation at a type is represented as a DTT type family but also permits expressing certain semantic definitions. We use the Edinburgh Logical Framework (LF) incarnation of DTT and implement our notion of logical relations in the type-checker Twelf. This enables us to formalize and mechanically decide the validity of logical relation arguments. Furthermore, our implementation includes a module system so that logical relations can be built modularly. We validate our approach by formalizing and verifying several syntactic and semantic meta-theorems in Twelf. Moreover, we show how object languages encoded in DTT can inherit a notion of logical relation from the logical framework. ©2013 ACM 1529-3785/2013/11- ART33 $15.00.
AB - Logical relations are a central concept used to study various higher-order type theories and occur frequently in the proofs of a wide variety of meta-theorems. Besides extending the logical relation principle to more general languages, an important research question has been how to represent and thus verify logical relation arguments in logical frameworks. We formulate a theory of logical relations for Dependent Type Theory (DTT) with β η-equality which guarantees that any valid logical relation satisfies the Basic Lemma. Our definition is syntactic and reflective in the sense that a relation at a type is represented as a DTT type family but also permits expressing certain semantic definitions. We use the Edinburgh Logical Framework (LF) incarnation of DTT and implement our notion of logical relations in the type-checker Twelf. This enables us to formalize and mechanically decide the validity of logical relation arguments. Furthermore, our implementation includes a module system so that logical relations can be built modularly. We validate our approach by formalizing and verifying several syntactic and semantic meta-theorems in Twelf. Moreover, we show how object languages encoded in DTT can inherit a notion of logical relation from the logical framework. ©2013 ACM 1529-3785/2013/11- ART33 $15.00.
UR - http://www.scopus.com/inward/record.url?scp=84890379779&partnerID=8YFLogxK
U2 - 10.1145/2536740.2536741
DO - 10.1145/2536740.2536741
M3 - Article
SN - 1529-3785
VL - 14
JO - ACM Transactions on Computational Logic
JF - ACM Transactions on Computational Logic
IS - 4
M1 - 32
ER -