Totally Beluga

Computation and Logic Group, McGill University, May 2013-August 2014.

Today, we routinely specify and reason about the runtime behaviour of software using formal systems such as type systems or logics for access control to establish safety properties. In our work, we concentrate on Beluga, a novel programming and proof environment which supports specifying formal systems in the logical framework LF via axioms and inference rules. It provides direct support for common and tricky routines dealing with variables, such as capture-avoiding substitution and renaming. Moreover, Beluga allows embedding contextual LF objects, i.e. a LF object together with the context in which it is meaningful, in programs.Img

Our work provides a foundation for writing total functions over contextual objects. More broadly, it provides an important, currently missing piece in the foundation of the proof and programming language Beluga since it justifies that well-founded recursive programs implement well-founded inductive proofs. The work has a wide range of implications and applications in certified programming, proof-carrying architectures, and mechanizing meta-theory of programming languages.


Related Works

Related Presentations



Leave a Reply