Nested abstract syntax in Coq

DOI10.1007/s10817-010-9207-9zbMath1260.68374OpenAlexW2147567862MaRDI QIDQ1945918

Marco Maggesi, Andre Hirschowitz

Publication date: 17 April 2013

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-010-9207-9

zbMATH Keywords

semanticsabstract syntax\texttt{Coq}nested datatypesPOPLmarkSystem \(\mathrm F _{ < :}\)

Mathematics Subject Classification ID

Theory of programming languages (68N15) Functional programming and lambda calculus (68N18)

Related Items (5)

Strongly typed term representations in Coq ⋮ A formalized general theory of syntax with bindings ⋮ Variable binding and substitution for (nameless) dummies ⋮ C-system of a module over a \(Jf\)-relative monad ⋮ A type- and scope-safe universe of syntaxes with binding: their semantics and proofs

Uses Software

• Coq
• PoplMark

Cites Work

• Unnamed Item
• Unnamed Item
• A new approach to abstract syntax with variable binding
• Modules over monads and initial semantics
• Towards a mechanized metatheory of standard ML
• Engineering formal metatheory
• Recursion on Nested Datatypes in Dependent Type Theory
• Nested Datatypes with Generalized Mendler Iteration: Map Fusion and the Example of the Representation of Untyped Lambda Calculus with Explicit Flattening
• Modules over Monads and Linearity
• An induction principle for nested datatypes in intensional type theory
• de Bruijn notation as a nested datatype
• Theorem Proving in Higher Order Logics

This page was built for publication: Nested abstract syntax in Coq