Higher-order abstract syntax in Coq
From MaRDI portal
Recommendations
- Higher-order abstract syntax in type theory
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- The theory of contexts for first order and higher order abstract syntax
- Two-level meta-reasoning in Coq
- Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq
Cited in
(50)- -calculus in (Co)inductive-type theory
- A formalized general theory of syntax with bindings
- Canonical HybridLF: extending Hybrid with dependent types
- Structural cut elimination. I: Intuitionistic and classical logic
- On the formalization of the modal -calculus in the calculus of inductive constructions
- Nested abstract syntax in Coq
- A formalized general theory of syntax with bindings: extended version
- \(\mathrm{HO}\pi\) in Coq
- Rensets and renaming-based recursion for syntax with bindings
- Mechanized metatheory revisited
- Formalization of metatheory of the Quipper quantum programming language in a linear logic
- Mechanizing focused linear logic in Coq
- Strongly typed term representations in Coq
- A two-level logic approach to reasoning about computations
- Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts
- A simple take on typed abstract syntax in Haskell-like languages
- Case analysis of higher-order data
- Developing (meta)theory of -calculus in the theory of contexts
- The theory of contexts for first order and higher order abstract syntax
- A Coq library for verification of concurrent programs
- Polymorphic Abstract Syntax via Grothendieck Construction
- Variable Binding, Symmetric Monoidal Closed Theories, and Bigraphs
- Focusing and higher-order abstract syntax
- Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq
- Syntax for Free: Representing Syntax with Binding Using Parametricity
- Higher-order abstract syntax in type theory
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- A fully adequate shallow embedding of the π-calculus in Isabelle/HOL with mechanized syntax analysis
- Two-level meta-reasoning in Coq
- Proof pearl: Abella formalization of \(\lambda \)-calculus cube property
- A focused linear logical framework and its application to metatheory of object logics
- Complete algebraic semantics for second-order rewriting systems based on abstract syntax with variable binding
- Encoding natural semantics in Coq
- POPLMark reloaded: mechanizing proofs by logical relations
- Parametric higher-order abstract syntax for mechanized semantics
- Initial semantics for higher-order typed syntax in \textsf{Coq}
- LF+ in Coq for "fast and loose" reasoning
- Higher-order abstract syntax in Isabelle/HOL
- The practice of logical frameworks
- Primitive recursion for higher-order abstract syntax
- A Survey of the Proof-Theoretic Foundations of Logic Programming
- Rensets and renaming-based recursion for syntax with bindings extended version
- A type checker for a logical framework with union and intersection types (system description)
- Mechanized metatheory revisited: an extended abstract (invited paper)
- An improved implementation and abstract interface for Hybrid
- A monadic formalization of ML5
- Two applications of logic programming to Coq
- An initial algebra approach to term rewriting systems with variable binders
- Mechanizing type environments in weak HOAS
- Nominal techniques in Isabelle/HOL
This page was built for publication: Higher-order abstract syntax in Coq
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3024831)
