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. If time permits, we will revisit the POPLMark Reloaded challenge we recently proposed together with researchers from Gothenburg University (Sweden), McGill University, University of Saarbruecken (Germany), Radboud University (Netherlands), and University of Milan (Italy).

To follow along, we suggest participants install Beluga from

https://github.com/Beluga-lang

Additional material for the tutorial will be posted at:

http://complogic.cs.mcgill.ca/beluga/