Beluga: Programming Proofs About Formal Systems

Beluga is a proof environment that provides a sophisticated infrastructure for implementing formal systems based on the logical framework LF together with a reasoning language for implementing (co)inductive proofs about them following the Curry-Howard isomorphism. The tutorial aims primarily at researchers in programming languages and provides a thorough introduction to Beluga and its underlying fundamental ideas of representing, manipulating and reasoning about open code / proof fragments.

By the end of the tutorial, participants will be able to encode their own language and implement proofs about it. We will walk participants through three case studies in the simply-typed lambda calculus: type uniqueness, weak normalization, and strong normalization. The walk-through will be given by Jacob Errington and Aliya Hameer using the Beluga interactive mode for Emacs.

Slides

Download the slides used in the presentation here.

Complete code examples used in the workshop

• Type uniqueness
• Weak normalization for STLC
• Strong normalization for STLC

Want to get involved?

There's lots to do! Visit our Github to get involved.