Reasoning with higher-order abstract syntax in a logical framework
From MaRDI portal
Publication:5738952
DOI10.1145/504077.504080zbMath1365.68164arXivcs/0003062OpenAlexW2099521332MaRDI QIDQ5738952
Raymond McDowell, Dale A. Miller
Publication date: 13 June 2017
Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/cs/0003062
Theory of programming languages (68N15) Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
Cut-elimination for quantified conditional logic, The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey, Functions-as-constructors higher-order unification: extended pattern unification, Nominal logic, a first order theory of names and binding, Term-Generic Logic, Nominal abstraction, Unnamed Item, Towards substructural property-based testing, Cut elimination for a logic with induction and co-induction, LINCX: A Linear Logical Framework with First-Class Contexts, The Abella Interactive Theorem Prover (System Description), On the Expressivity of Minimal Generic Quantification, Reasoning in Abella about Structural Operational Semantics Specifications, Formalizing Operational Semantic Specifications in Logic, Mechanized metatheory revisited, Encoding Generic Judgments, A proof theory for model checking, Formalization of metatheory of the Quipper quantum programming language in a linear logic, Formal meta-level analysis framework for quantum programming languages, Term-generic logic, A focused linear logical framework and its application to metatheory of object logics
