Beluga: Establishing Trustworthy Computing through Programming Proofs


Software systems should be robust, reliable, and predictable. A
key step towards a safe and trustworthy infrastructure is verifying
compliance of the software with a formal software policy. However,
verifying complex safety properties in existing programming and
proof environments can be costly and time consuming, as we need to
repeatedly build up low-level infrastructure from scratch and using
it in formal developments is tedious and error prone. 

The Beluga project aims to change the way we develop and implement
safe software systems by extending a general purpose programming and
proof language with the ability to directly represent and manipulate
formal systems and proofs. To specify formal systems and represent
derivations within them, Beluga relies on the logical framework LF;
to reason about formal systems, Beluga provides a dependently typed
functional language for implementing (co)inductive proofs about
derivation trees as (co)recursive functions following the Curry-Howard
isomorphism. Key to this approach is the ability to model derivation
trees that depend on a context of assumptions using a generalization
of the logical framework LF, i.e. contextual LF which supports
first-class contexts and (simultaneous) substitutions. Using several
examples, I show how Beluga enables direct and compact mechanizations
of the meta-theory of formal systems, in particular programming
languages and logics, and outline several future research directions.


Bio

Brigitte Pientka is an Associate Professor in the School of Computer
Science at McGill University, Montreal, Canada. She received her Ph.D.
from Carnegie Mellon University (Pittsburgh, USA) in 2003. Currently,
she is a Humboldt Research Fellow at the Ludwig-Maximilian  University
Munich, Germany. Her research interest lies in developing a theoretical
and practical foundation for building and reasoning about reliable safe
software systems. To achieve this goal, she combines theoretical
research on the logical foundations of computer science in programming
languages and verification with system building.