A Modular Approach to Metatheoretic Reasoning for Extensible Languages
summary
Claims a practical, sound method to build complete metatheory for languages assembled from independently written extensions by: decomposing proofs around fragments, using projection constraints to relate extension syntax to the host, and automatically composing modular proofs into whole-language proofs. Implements a language-spec system Sterling and a proof tool Extensibella that emits machine-checkable Abella proofs. Distinguishes foundational vs auxiliary properties and documents which proof restrictions (case-analysis limits) are required for guaranteed composability.
AI-written summary · about
chapters (11)
- 0:00Modular metatheoretic reasoning
- 1:58Language extensibility framework
- 4:03Why modular metatheory matters
- 5:50Foundational vs auxiliary properties
- 7:54Modular proofs for auxiliary properties
- 10:20Projection constraints impact
- 12:30Comparison with prior work
- 13:57Open language libraries
- 14:41Framework implementation
- 16:07Future work and testing
- 17:10Q&A
related talks
16mA metalanguage for multi-phase modularity
20mOn Extending Incorrectness Logic with Backwards Reasoning
20mUnifying compositional verification and certified compilation with a three-dimensional(…)
21mMechanised Hypersafety Proofs about Structured Data
41mA Modular Compositional Approach to Engineering Complex Systems
11mMorello Cerise: proving secure encapsulation (work in progress)
23mSeparating the Wheat from the Chaff: Understanding (In-)Completeness of Proof(…)
31mCooperative Specification via Composition Control