Brigitte Pientka
Associate Professor in the School of Computer Science at McGill University, Montreal, Canada
Programming Proofs in Context
Abstract:
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.
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 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.