Rabe F, Roux N (2021)
Publication Type: Conference contribution
Publication year: 2021
Publisher: Open Publishing Association
Book Volume: 337
Pages Range: 88-103
Conference Proceedings Title: Electronic Proceedings in Theoretical Computer Science, EPTCS
Event location: Pittsburgh, PA, USA
DOI: 10.4204/EPTCS.337.7
Type theories can be formalized using the intrinsically (hard) or the extrinsically (soft) typed style. In large libraries of type theoretical features, often both styles are present, which can lead to code duplication and integration issues. We define an operator that systematically translates a hard-typed into the corresponding softtyped formulation. Even though this translation is known in principle, a number of subtleties make it more difficult than naively expected. Importantly, our translation preserves modularity, i.e., it maps structured sets of hard-typed features to correspondingly structured soft-typed ones. We implement our operator in the MMT system and apply it to a library of type-theoretical features.
APA:
Rabe, F., & Roux, N. (2021). Systematic translation of formalizations of type theory from intrinsic to extrinsic style. In Elaine Pimentel, Enrico Tassi (Eds.), Electronic Proceedings in Theoretical Computer Science, EPTCS (pp. 88-103). Pittsburgh, PA, USA: Open Publishing Association.
MLA:
Rabe, Florian, and Navid Roux. "Systematic translation of formalizations of type theory from intrinsic to extrinsic style." Proceedings of the 16th Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2021, Pittsburgh, PA, USA Ed. Elaine Pimentel, Enrico Tassi, Open Publishing Association, 2021. 88-103.
BibTeX: Download