
TL;DR
This paper introduces a generic framework for well-typed syntaxes that reduces boilerplate code and proofs, inspired by algebraic approaches, to streamline the development of formal systems.
Contribution
It presents a novel signature-axiom framework that abstracts boilerplate code and proofs in defining and working with well-typed syntaxes.
Findings
Framework effectively reduces boilerplate in syntax definitions
Generalizes common proofs in syntax manipulation
Provides a structured algebraic approach to syntax
Abstract
This article explores a generic framework of well-typed and well-scoped syntaxes, with a signature-axiom approach resembling traditional abstract algebra. The boilerplate code needed in defining operations on syntaxes is identified and abstracted away. Some of the frequent boilerplate proofs are also generalized.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Logic, Reasoning, and Knowledge
