Brigitte Pientka
Associate Professor in the School of Computer Science at McGill University, Montreal, Canada

Programming Proofs in Context

Today, we routinely reason about the runtime  behavior of software using formal systems such as type systems or logics for access control or information flow to establish safety and liveness properties.

In this talk, I will survey Beluga, a dependently typed programming and proof environment. It supports specifying formal systems in the logical framework LF and directly supports common and tricky routines dealing with variables, such as capture-avoiding substitution and renaming. Moreover, Beluga allows embedding LF objects together with their surrounding context in programs and
supports recursive types to state properties about LF objects and their contexts. Using two examples, a type-preserving evaluator using closures and a weak normalization proof, I will highlight several key aspects of Beluga and its
design. Taken together these examples demonstrate the elegance and conciseness of Beluga for specifying, verifying and validating proofs.

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 in 2003 working with Frank Pfenning.   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.  

Thursday, May, 8th, 2014
2:00 PM
Gates & Hillman Centers 8102

Principles of Programming Seminars