Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2018.19
URN: urn:nbn:de:0030-drops-91891
URL: https://drops.dagstuhl.de/opus/volltexte/2018/9189/
Jacob-Rao, Rohan ; Pientka, Brigitte ; Thibodeau, David
Index-Stratified Types
| pdf-format: |
|
Abstract
We present Tores, a core language for encoding metatheoretic proofs. The novel features we introduce are well-founded Mendler-style (co)recursion over indexed data types and a form of recursion over objects in the index language to build new types. The latter, which we call index-stratified types, are analogue to the concept of large elimination in dependently typed languages. These features combined allow us to encode sophisticated case studies such as normalization for lambda calculi and normalization by evaluation. We prove the soundness of Tores as a programming and proof language via the key theorems of subject reduction and termination.
BibTeX - Entry
@InProceedings{jacobrao_et_al:LIPIcs:2018:9189,
author = {Rohan Jacob-Rao and Brigitte Pientka and David Thibodeau},
title = {{Index-Stratified Types}},
booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
pages = {19:1--19:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-077-4},
ISSN = {1868-8969},
year = {2018},
volume = {108},
editor = {H{\'e}l{\`e}ne Kirchner},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2018/9189},
URN = {urn:nbn:de:0030-drops-91891},
doi = {10.4230/LIPIcs.FSCD.2018.19},
annote = {Keywords: Indexed types, (co)recursive types, logical relations}
}
| Keywords: | Indexed types, (co)recursive types, logical relations | |
| Seminar: | 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018) | |
| Issue date: | 2018 | |
| Date of publication: | 04.07.2018 |
