Well-Founded Recursion over Contextual Objects ...

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 consi...

Full description

Bibliographic Details
Main Authors: Pientka, Brigitte, Abel, Andreas
Format: Conference Object
Language:English
Published: Schloss Dagstuhl – Leibniz-Zentrum für Informatik 2015
Subjects:
Type systems
Dependent Types
Logical Frameworks
Lambda
Beluga
Beluga*
Online Access:https://dx.doi.org/10.4230/lipics.tlca.2015.273
https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.273
Description
Summary: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. ... : LIPIcs, Vol. 38, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015), pages 273-287 ...

Similar Items