GMeta: A Generic Formal Metatheory Framework for First-Order Representations
Abstract elided by the publisher.
Related papers
- Formal metatheory of second-order abstract syntax POPL 2022
- Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk) CPP 2019
- Mechanizing metatheory in a logical framework JFP 2007
- Towards a mechanized metatheory of standard ML POPL 2007
- Foundational extensible corecursion: a proof assistant perspective ICFP 2015
- Constructive Galois connections: taming the Galois connection framework for mechanized metatheory ICFP 2016
- Leapfrog: certified equivalence for protocol parsers PLDI 2022
- Zooid: a DSL for certified multiparty computation: from mechanised metatheory to certified multiparty processes PLDI 2021