Abstract syntax for variable binders: An overview

DOI10.1007/3-540-44957-4_16MaRDI QIDQ2767057zbMATH OpenFDO

Authors Dale Miller

Publication date 28 January 2002

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-44957-4_16

Mathematics Subject Classification ID

Logic programming (68N17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Higher-order abstract syntax in Isabelle/HOL
• A new approach to abstract syntax with variable binding
• Higher-order substitutions
• Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq

Cited in

(15)

• Incorporating quotation and evaluation into Church's type theory
• The abstract variable-binding calculus
• A two-level logic approach to reasoning about computations
• A higher-order abstract syntax approach to verified transformations on functional programs
• On the expressivity of minimal generic quantification
• Encoding generic judgments: preliminary results
• scientific article; zbMATH DE number 3848593 (Why is no real title available?)
• The Abella Interactive Theorem Prover (System Description)
• Free variables and subexpressions in higher-order meta logic
• Constraint handling rules with binders, patterns and generic quantification
• Formalizing operational semantic specifications in logic
• Using circular programs for higher-order syntax (functional pearl)
• scientific article; zbMATH DE number 7649978 (Why is no real title available?)
• Nominal abstraction
• A new approach to abstract syntax with variable binding

This page was built for publication: Abstract syntax for variable binders: An overview

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