Inductive Beluga: Programming Proofs
BELUGA is a proof environment that provides a rich 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 descr...
| Main Authors: | , |
|---|---|
| Other Authors: | |
| Format: | Text |
| Language: | English |
| Subjects: | |
| Online Access: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.671.8795 http://www.cs.mcgill.ca/%7Ebpientka/papers/inductive-beluga.pdf |
| Summary: | BELUGA is a proof environment that provides a rich 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 that significantly increases beluga’s expressive power 3) we provide a totality checker that guarantees that recursive programs are well-founded and correspond to inductive proofs 4) we describe an interactive program development environment. Taken together these ex-tensions enable direct and compact mechanizations. To demonstrate bel-uga’s strength and illustrate these new features we develop a weak normalization proof using logical relations. |
|---|