Well-founded Recursion over Contextual Objects
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 cons...
| Main Authors: | , |
|---|---|
| Other Authors: | |
| Format: | Text |
| Language: | English |
| Subjects: | |
| 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 |
| Summary: | 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. |
|---|