Logical relations for a logical framework

Florian Rabe, Kristina Sojakova

Research output: Contribution to JournalArticleAcademicpeer-review

Abstract

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.
Original languageEnglish
Article number32
JournalACM Transactions on Computational Logic
Volume14
Issue number4
DOIs
Publication statusPublished - Nov 2013
Externally publishedYes

Fingerprint

Dive into the research topics of 'Logical relations for a logical framework'. Together they form a unique fingerprint.

Cite this