Higher-order abstract syntax in Isabelle/HOL

DOI10.1007/978-3-642-14052-5_33MaRDI QIDQ5747671zbMATH OpenOpenAlexFDO

Authors Douglas J. Howe

Publication date 14 September 2010

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-14052-5_33

Mathematics Subject Classification ID

Recommendations

• A fully adequate shallow embedding of the π-calculus in Isabelle/HOL with mechanized syntax analysis
• scientific article; zbMATH DE number 1701361
• Parametric higher-order abstract syntax for mechanized semantics
• Two-level hybrid: a system for reasoning using higher-order abstract syntax
• scientific article; zbMATH DE number 2185657

Cited in

(21)

• HasCasl: integrated higher-order specification and program development
• Nested abstract syntax in Coq
• Formalizing adequacy: a case study for higher-order abstract syntax
• scientific article; zbMATH DE number 1696799 (Why is no real title available?)
• scientific article; zbMATH DE number 1701361 (Why is no real title available?)
• Polymorphic Abstract Syntax via Grothendieck Construction
• The representational adequacy of Hybrid
• Focusing and higher-order abstract syntax
• A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
• Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq
• scientific article; zbMATH DE number 1301856 (Why is no real title available?)
• A fully adequate shallow embedding of the π-calculus in Isabelle/HOL with mechanized syntax analysis
• scientific article; zbMATH DE number 7204430 (Why is no real title available?)
• Parametric higher-order abstract syntax for mechanized semantics
• Boxes go bananas: encoding higher-order abstract syntax with parametric polymorphism
• Automated Deduction – CADE-20
• Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism
• Practical Programming with Higher-Order Encodings and Dependent Types
• scientific article; zbMATH DE number 7649970 (Why is no real title available?)
• Nominal techniques in Isabelle/HOL
• Abstract deduction and inferential models for type theory

Describes a project that uses

Uses Software

• Isabelle
• Isabelle/HOL

This page was built for publication: Higher-order abstract syntax in Isabelle/HOL

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