Well-founded Recursion over Contextual Objects

• Main Authors: Brigitte Pientka, Andreas Abel
• Other Authors: The Pennsylvania State University CiteSeerX Archives
• Format: Text
• Language: English
• Subjects: Dependent Types; Logical Frameworks Digital Object Identifier 10.4230/LIPIcs.xxx.yyy.p; Beluga; Beluga*
• Online Access: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.679.2929; http://www2.tcs.ifi.lmu.de/%7Eabel/tlca15-long.pdf

We present a core programming language that supports writing well-founded structurally recur-sive 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 methodol-ogy 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.