Nested abstract syntax in Coq

DOI10.1007/S10817-010-9207-9zbMATH Open1260.68374OpenAlexW2147567862MaRDI QIDQ1945918FDOQ1945918

André Hirschowitz, Marco Maggesi

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Theorem Proving in Higher Order Logics
• A new approach to abstract syntax with variable binding
• 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
• An induction principle for nested datatypes in intensional type theory
• de Bruijn notation as a nested datatype
• Modules over monads and initial semantics
• Modules over Monads and Linearity

Cited In (5)

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

Uses Software

• Coq
• PoplMark

Recommendations

• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• Inductive and coinductive components of corecursive functions in Coq 👍 👎
• Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq 👍 👎
• Structural Abstract Interpretation: A Formal Study Using Coq 👍 👎
• Higher-Order Abstract Syntax in Isabelle/HOL 👍 👎
• Towards Rewriting in Coq 👍 👎
• Initial Semantics for higher-order typed syntax in Coq 👍 👎

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

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