Parametric higher-order abstract syntax for mechanized semantics
From MaRDI portal
Publication:5178760
DOI10.1145/1411204.1411226zbMath1323.68184OpenAlexW4246086292MaRDI QIDQ5178760
Publication date: 16 March 2015
Published in: Proceedings of the 13th ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/1411204.1411226
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (27)
A linear logic framework for multimodal logics ⋮ A Functional Abstraction of Typed Invocation Contexts ⋮ Strongly typed term representations in Coq ⋮ Verifying Selective CPS Transformation for Shift and Reset ⋮ A formalized general theory of syntax with bindings ⋮ Rensets and renaming-based recursion for syntax with bindings extended version ⋮ Mechanizing type environments in weak HOAS ⋮ Formalized meta-theory of sequent calculi for linear logics ⋮ A strong call-by-need calculus ⋮ POPLMark reloaded: Mechanizing proofs by logical relations ⋮ Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax ⋮ The calculus of dependent lambda eliminations ⋮ Unnamed Item ⋮ A presheaf model of parametric type theory ⋮ Programs Using Syntax with First-Class Binders ⋮ A formalized general theory of syntax with bindings: extended version ⋮ Canonical HybridLF: extending Hybrid with dependent types ⋮ Is Impredicativity Implicitly Implicit ⋮ Combining deep and shallow embedding of domain-specific languages ⋮ Syntax for Free: Representing Syntax with Binding Using Parametricity ⋮ Mechanizing the Metatheory of mini-XQuery ⋮ Mechanized metatheory revisited ⋮ Formal meta-level analysis framework for quantum programming languages ⋮ Mechanizing focused linear logic in Coq ⋮ Rensets and renaming-based recursion for syntax with bindings ⋮ 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
Uses Software
This page was built for publication: Parametric higher-order abstract syntax for mechanized semantics
