article · ACM Transactions on Computational Logic · 2013

Logical relations for a logical framework

Cited by 7Abstract and details only

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.

Cite this paper

APA 7

Rabe, F., & Sojakova, K. (2013). Logical relations for a logical framework. ACM Transactions on Computational Logic, 14(4), 1–34. https://doi.org/10.1145/2536740.2536741

MLA 9

Rabe, Florian, and Kristina Sojakova. “Logical relations for a logical framework.” ACM Transactions on Computational Logic, vol. 14, no. 4, 2013, pp. 1–34, https://doi.org/10.1145/2536740.2536741.

Chicago

Rabe, Florian, and Kristina Sojakova. 2013. “Logical relations for a logical framework.” ACM Transactions on Computational Logic 14 (4): 1–34. https://doi.org/10.1145/2536740.2536741.

Harvard

Rabe, F. and Sojakova, K. (2013) ‘Logical relations for a logical framework’, ACM Transactions on Computational Logic, 14(4), pp. 1–34. Available at: https://doi.org/10.1145/2536740.2536741.

BibTeX

@article{rabe2013logical,
  title = {{Logical relations for a logical framework}},
  author = {Rabe, Florian and Sojakova, Kristina},
  journal = {ACM Transactions on Computational Logic},
  volume = {14},
  number = {4},
  pages = {1--34},
  year = {2013},
  doi = {10.1145/2536740.2536741}
}

Made from the index record. Check names, capitalisation and page numbers against the paper. Need another style? AI for Research has over 10,000.