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 normalization proof using logical relations.