Every proof assistant: Beluga
source link: http://math.andrej.com/2020/05/25/mechanizing-meta-theory-in-beluga/
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
Every proof assistant: Beluga
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: BelugaAbstract: 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:
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.
Name
Website
Comment
Recommend
About Joyk
Aggregate valuable and interesting links.
Joyk means Joy of geeK