Automatically Generated Infrastructure for De Bruijn Syntaxes

DOI10.1007/978-3-642-39634-2_29zbMath1317.68228OpenAlexW184345177MaRDI QIDQ5327359

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 assistantformalizationde Bruijn syntaxinfrastructure generation

Mathematics Subject Classification ID

Theory of programming languages (68N15)

Related Items (2)

A formalized general theory of syntax with bindings: extended version ⋮ A type- and scope-safe universe of syntaxes with binding: their semantics and proofs

Uses Software

• Coq
• Gmeta

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