Write a Blog >>
ICFP 2018
Sun 23 - Sat 29 September 2018 St. Louis, Missouri, United States

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


Additional material for the tutorial will be posted at:


Fri 28 Sep

Displayed time zone: Guadalajara, Mexico City, Monterrey change

13:00 - 16:00
T04: Beluga: Programming Proofs About Formal SystemsTutorials at Texas Special
Chair(s): Jacob Thomas Errington McGill University, Aliya Hameer McGill University, Brigitte Pientka McGill University
T04: Beluga: Programming Proofs About Formal Systems
Brigitte Pientka McGill University, Jacob Thomas Errington McGill University, Aliya Hameer McGill University