Brigitte Pientka (McGill University, Canada)

Programming Logical Relations Proofs

Abstract: 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 the mechanization of the 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.