Formal Metatheory of Second-Order Abstract Syntax
View / Open Files
Conference Name
Annual Symposium on Principles of Programming Languages
Type
Conference Object
This Version
AM
Metadata
Show full item recordCitation
Fiore, M., & Szamozvancev, D. Formal Metatheory of Second-Order Abstract Syntax. Annual Symposium on Principles of Programming Languages. https://doi.org/10.17863/CAM.78103
Abstract
Despite extensive research both on the theoretical and practical fronts, formalising, reasoning about, and implementing languages with variable binding is still a daunting endeavour – repetitive boilerplate and the overly complicated metatheory of capture-avoiding substitution often get in the way of progressing on to the actually interesting properties of a language. Existing developments offer some relief, however at the expense of inconvenient and error-prone term encodings and lack of formal foundations. We present a mathematically-inspired language-formalisation framework implemented in Agda. The system translates the description of a syntax signature with variable-binding operators into an intrinsically-encoded, inductive data type equipped with syntactic operations such as weakening and substitution, along with their correctness properties. The generated metatheory further incorporates metavariables and their associated operation of metasubstitution, which enables second-order equational/rewriting reasoning. The underlying mathematical foundation of the framework – initial algebra semantics – derives compositional interpretations of languages into their models satisfying the semantic substitution lemma by construction.
Sponsorship
EPSRC (EP/V002309/1)
EPSRC (2119874)
Identifiers
External DOI: https://doi.org/10.17863/CAM.78103
This record's URL: https://www.repository.cam.ac.uk/handle/1810/330658
Statistics
Total file downloads (since January 2020). For more information on metrics see the
IRUS guide.
Recommended or similar items
The current recommendation prototype on the Apollo Repository will be turned off on 03 February 2023. Although the pilot has been fruitful for both parties, the service provider IKVA is focusing on horizon scanning products and so the recommender service can no longer be supported. We recognise the importance of recommender services in supporting research discovery and are evaluating offerings from other service providers. If you would like to offer feedback on this decision please contact us on: support@repository.cam.ac.uk