# Every proof assistant: Beluga

- 25 May 2020
- Talks, Every proof assistant

We are marching on with the Every proof assistant series!

## Mechanizing Meta-Theory in Beluga

Time:Thursday, May 28, 2020 from 16:00 to 17:00 (Central European Summer Time, UTC+2)

Location:online at Zoom ID 989 0478 8985

Speaker:Brigitte Pientka (McGill University)

Proof assistant:Beluga

Abstract:Mechanizing formal systems, given via axioms and inference rules, together with proofs about them plays an important role in establishing trust in formal developments. In this talk, I will survey the proof environment Beluga. To specify formal systems and represent derivations within them, Beluga relies on the logical framework LF; to reason about formal systems, Beluga provides a dependently typed functional language for implementing (co)inductive proofs about derivation trees as (co)recursive functions following the Curry-Howard isomorphism. Key to this approach is the ability to model derivation trees that depend on a context of assumptions using a generalization of the logical framework LF, i.e. contextual LF which supports first-class contexts and simultaneous substitutions.Our experience demonstrated that Beluga enables direct and compact mechanizations of the meta-theory of formal systems, in particular programming languages and logics.

Upcoming talks:

- June 4, 2020: Jon Sterling - redtt
- June 11, 2020: Conor McBride - Epigram 2
- June 25, 2020: William J. Bowman, Cur
- July 2, 2020: Anders Mörtberg - Cubical Agda

##### Post a comment:

`$⋯$`

for inline and `$$⋯$$`

for display LaTeX formulas,
and `<pre>⋯</pre>`

for display code. Your E-mail address is only used to compute
your Gravatar and is not stored anywhere.
Comments are moderated through pull requests.