Inductive Beluga: Programming Proofs

5 years 2 months ago
Inductive Beluga: Programming Proofs
Abstract. beluga is a proof environment which provides a sophisticated infrastructure for implementing formal systems based on the logical framework LF together with a first-order reasoning language for implementing inductive proofs about them following the Curry-Howard isomorphism. In this paper we describe four significant extensions to beluga: 1) we enrich our infrastructure for modelling formal systems with first-class simultaneous substitutions, a key and common concept when reasoning about formal systems 2) we support inductive definitions in our reasoning language which significantly increases beluga’s expressive power 3) we provide a totality checker which guarantees that recursive programs are well-founded and correspond to inductive proofs 4) we describe an interactive program development environment. Taken together these extensions enable direct and compact mechanizations. To demonstrate beluga’s strength and illustrate these new features we develop a weak normaliza...
Brigitte Pientka, Andrew Cave
Added 17 Apr 2016
Updated 17 Apr 2016
Type Journal
Year 2015
Where CADE
Authors Brigitte Pientka, Andrew Cave
Comments (0)