Software systems should be robust, reliable, and predictable. 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 context in programs and types supporting inductive
and coinductive definitions. I will discuss how to write inductive and
coinductive proofs about LF specifications using three different examples: type
uniqueness, normalization by evaluation, and the fact that evaluating a
lambda-term cannot yield a value and diverge at the same time. Taken together
these examples demonstrate the elegance and conciseness of Beluga for
specifying, verifying and validating safety properties.