License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TLCA.2015.273
URN: urn:nbn:de:0030-drops-51699
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5169/
Pientka, Brigitte ;
Abel, Andreas
Well-Founded Recursion over Contextual Objects
Abstract
We present a core programming language that supports writing well-founded structurally recursive functions using simultaneous pattern matching on contextual LF objects and contexts. The main technical tool is a coverage checking algorithm that also generates valid recursive calls. To establish consistency, we define a call-by-value small-step semantics and prove that every well-typed program terminates using a reducibility semantics. Based on the presented methodology we have implemented a totality checker as part of the programming and proof environment Beluga where it can be used to establish that a total Beluga program corresponds to a proof.
BibTeX - Entry
@InProceedings{pientka_et_al:LIPIcs:2015:5169,
author = {Brigitte Pientka and Andreas Abel},
title = {{Well-Founded Recursion over Contextual Objects}},
booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
pages = {273--287},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-87-3},
ISSN = {1868-8969},
year = {2015},
volume = {38},
editor = {Thorsten Altenkirch},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2015/5169},
URN = {urn:nbn:de:0030-drops-51699},
doi = {10.4230/LIPIcs.TLCA.2015.273},
annote = {Keywords: Type systems, Dependent Types, Logical Frameworks}
}
Keywords: |
|
Type systems, Dependent Types, Logical Frameworks |
Collection: |
|
13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015) |
Issue Date: |
|
2015 |
Date of publication: |
|
15.06.2015 |