Logic Column 16: Higher-Order Abstract Syntax: Setting the Record Straight
Karl Crary, Robert Harper
TL;DR
This paper clarifies and defends the use of higher-order abstract syntax in formal logic, addressing previous critiques and setting the record straight on its validity and applications.
Contribution
It provides a detailed rebuttal to criticisms of higher-order abstract syntax, reaffirming its correctness and usefulness in logical frameworks.
Findings
Clarifies misconceptions about higher-order abstract syntax
Reaffirms the correctness of higher-order abstract syntax
Addresses specific critiques from previous literature
Abstract
This article responds to a critique of higher-order abstract syntax appearing in Logic Column 14, ``Nominal Logic and Abstract Syntax'', cs.LO/0511025.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Logic, Reasoning, and Knowledge · Formal Methods in Verification