Parametric higher-order abstract syntax for mechanized semantics
From MaRDI portal
Recommendations
Cited in
(44)- A formalized general theory of syntax with bindings
- Canonical HybridLF: extending Hybrid with dependent types
- Combining deep and shallow embedding of domain-specific languages
- A formalized general theory of syntax with bindings: extended version
- Rensets and renaming-based recursion for syntax with bindings
- Mechanized metatheory revisited
- Formal meta-level analysis framework for quantum programming languages
- Mechanizing focused linear logic in Coq
- Strongly typed term representations in Coq
- Formalized meta-theory of sequent calculi for linear logics
- A higher-order abstract syntax approach to verified transformations on functional programs
- Programs using syntax with first-class binders
- Mechanizing the metatheory of mini-XQuery
- 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 type- and scope-safe universe of syntaxes with binding: their semantics and proofs
- A focused linear logical framework and its application to metatheory of object logics
- A Functional Abstraction of Typed Invocation Contexts
- Verifying selective CPS transformation for shift and reset
- POPLMark reloaded: mechanizing proofs by logical relations
- Programming type-safe transformations using higher-order abstract syntax
- Boxes go bananas: encoding higher-order abstract syntax with parametric polymorphism
- The calculus of dependent lambda eliminations
- Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism
- Higher-order abstract syntax in Isabelle/HOL
- Parametric compositional data types
- A linear logic framework for multimodal logics
- A presheaf model of parametric type theory
- Is Impredicativity Implicitly Implicit
- Rensets and renaming-based recursion for syntax with bindings extended version
- scientific article; zbMATH DE number 7809762 (Why is no real title available?)
- Certifying CPS transformation of let-polymorphic calculus using PHOAS
- Towards a scalable proof engine: a performant Prototype rewriting primitive for Coq
- Mechanized metatheory revisited: an extended abstract (invited paper)
- Abstractions for multi-sorted substitutions
- Structured monads for generic first-order syntax metatheory
- Abstract representation of binders in OCaml using the Bindlib library
- Countability of inductive types formalized in the object-logic level
- Facilitating meta-theory reasoning (invited paper)
- Syntax monads for the working formal metatheorist
- Two applications of logic programming to Coq
- Modular abstract syntax trees (MAST): substitution tensors with second-class sorts
- Mechanizing type environments in weak HOAS
This page was built for publication: Parametric higher-order abstract syntax for mechanized semantics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5178760)
