Automatically Generated Infrastructure for De Bruijn Syntaxes

DOI10.1007/978-3-642-39634-2_29MaRDI QIDQ5327359zbMATH OpenOpenAlexFDO

Authors E. Polonowski

Publication date 7 August 2013

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-39634-2_29

zbMATH Keywords

Coq proof assistantde Bruijn syntaxformalizationinfrastructure generation

Mathematics Subject Classification ID

Theory of programming languages (68N15)

Recommendations

• Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions
• GENERATION OF LANGUAGES BY REWRITING SYSTEMS THAT RESEMBLE AUTOMATA
• Automated Generation of BSP Automata
• scientific article; zbMATH DE number 5048474
• scientific article; zbMATH DE number 3999321
• Constructive system for automatic program synthesis
• Synthesis for Structure Rewriting Systems
• SMT-based generation of symbolic automata

Cited in

(5)

• A formalized general theory of syntax with bindings: extended version
• Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions
• A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
• Countability of inductive types formalized in the object-logic level
• Modular abstract syntax trees (MAST): substitution tensors with second-class sorts

Describes a project that uses

Uses Software

• Coq
• Gmeta

This page was built for publication: Automatically Generated Infrastructure for De Bruijn Syntaxes

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5327359)