Organizer: MAIS Graduate Seminar
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.
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.