Parametric higher-order abstract syntax for mechanized semantics

DOI10.1145/1411204.1411226zbMath1323.68184OpenAlexW4246086292MaRDI QIDQ5178760

Adam Chlipala

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

zbMATH Keywords

dependent typescompiler verificationinteractive proof assistantstype-theoretic semantics

Mathematics Subject Classification ID

Theory of programming languages (68N15) Theory of compilers and interpreters (68N20) Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55)

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

• Unnamed Item
• Unnamed Item

This page was built for publication: Parametric higher-order abstract syntax for mechanized semantics