Systematic Translation of Formalizations of Type Theory from Intrinsic to Extrinsic Style
Autor: | Florian Rabe, Navid Roux |
---|---|
Rok vydání: | 2021 |
Předmět: |
FOS: Computer and information sciences
Computer Science - Logic in Computer Science Modularity (networks) Operator (computer programming) Type theory Theoretical computer science Computer science Duplicate code Type (model theory) Translation (geometry) Logic in Computer Science (cs.LO) Style (sociolinguistics) |
Zdroj: | Electronic Proceedings in Theoretical Computer Science. 337:88-103 |
ISSN: | 2075-2180 |
Popis: | 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 soft-typed 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. Comment: In Proceedings LFMTP 2021, arXiv:2107.07376 |
Databáze: | OpenAIRE |
Externí odkaz: |