Documentation

If you have trouble discerning Beluga code from older releases, consult the legacy syntax for clarification.

Guides:

• Beluga reference guide
• Beginner's Guide to Programming in Beluga
• For Beginners
• For Intermediate Users
• For Advanced Users

Tutorials:

• Beluga: Programming Proofs About Formal Systems (ICFP-18 Tutorial), September 2018
• Mechanizing Meta-Theory in Beluga (CADE-25 Tutorial), August 2015
• Mechanizing Types and Programming Languages: A Companion (Draft from 24 July, 2015): This is a companion that loosely follows B. Pierce's book "Types and Programming Languages" and shows how to mechanize the material in Beluga. The code to the companion is available on GitHub (see beluga-code)
  For an up-to-date version or to contribute see our GitHub repository.

Overview Talks:

• Mechanizing Meta-Theory in Beluga, 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015), June 2015
• Programming logical relations proofs, Brigitte Pientka, Certification of high-level and low-level programs, Institut Henri Poincare, Paris, France, June 2014 (slides)
• Beluga-mu: Programming proofs in context, Brigitte Pientka, POP Seminar, Carnegie Mellon University, May 2014 (slides)
• Beluga-mu: Programming proofs in context, Brigitte Pientka, Invited talk at International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'12). (slides)

Publications

For more readings please visit Prof. Brigitte Pientka's publications here: https://www.cs.mcgill.ca/~bpientka/research.html.

© Computation and Logic Group
Department of Computer Science, McGill University
3480 University Street, Montreal, Quebec, Canada, H3A 0E9