Reasoning with higher-order abstract syntax in a logical framework
From MaRDI portal
Publication:5738952
Abstract: Logical frameworks based on intuitionistic or linear logics with higher-type quantification have been successfully used to give high-level, modular, and formal specifications of many important judgments in the area of programming languages and inference systems. Given such specifications, it is natural to consider proving properties about the specified systems in the framework: for example, given the specification of evaluation for a functional programming language, prove that the language is deterministic or that evaluation preserves types. One challenge in developing a framework for such reasoning is that higher-order abstract syntax (HOAS), an elegant and declarative treatment of object-level abstraction and substitution, is difficult to treat in proofs involving induction. In this paper, we present a meta-logic that can be used to reason about judgments coded using HOAS; this meta-logic is an extension of a simple intuitionistic logic that admits higher-order quantification over simply typed lambda-terms (key ingredients for HOAS) as well as induction and a notion of definition. We explore the difficulties of formal meta-theoretic analysis of HOAS encodings by considering encodings of intuitionistic and linear logics, and formally derive the admissibility of cut for important subsets of these logics. We then propose an approach to avoid the apparent tradeoff between the benefits of higher-order abstract syntax and the ability to analyze the resulting encodings. We illustrate this approach through examples involving the simple functional and imperative programming languages PCF and PCF:=. We formally derive such properties as unicity of typing, subject reduction, determinacy of evaluation, and the equivalence of transition semantics and natural semantics presentations of evaluation.
Recommendations
- Reasoning with higher-order abstract syntax and contexts: a comparison
- scientific article; zbMATH DE number 1696789
- scientific article; zbMATH DE number 1863386
- scientific article; zbMATH DE number 3988745
- scientific article; zbMATH DE number 1926604
- Proof-theoretic and higher-order extensions of logic programming
- A practical framework for theabstract interpretation of logic programs
- scientific article; zbMATH DE number 1956525
Cited in
(45)- Nominal logic, a first order theory of names and binding
- Cut elimination for a logic with induction and co-induction
- Functions-as-constructors higher-order unification: extended pattern unification
- Mechanized metatheory revisited
- 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
- Cut-elimination for quantified conditional logic
- A normative model of classical reasoning in higher order languages
- scientific article; zbMATH DE number 1670748 (Why is no real title available?)
- On the expressivity of minimal generic quantification
- Reasoning in Abella about structural operational semantics specifications
- Encoding generic judgments: preliminary results
- Comparing higher-order encodings in logical frameworks and tile logic
- Higher-order syntax and saturation algorithms for hybrid logic
- Two-level hybrid: a system for reasoning using higher-order abstract syntax
- The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
- \textsc{Lincx}: a linear logical framework with first-class contexts
- Term-Generic Logic
- Focusing and higher-order abstract syntax
- Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF
- The Abella Interactive Theorem Prover (System Description)
- A framework for defining logics
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- scientific article; zbMATH DE number 1942465 (Why is no real title available?)
- scientific article; zbMATH DE number 1956525 (Why is no real title available?)
- scientific article; zbMATH DE number 1927412 (Why is no real title available?)
- scientific article; zbMATH DE number 1927423 (Why is no real title available?)
- Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions
- Formalizing operational semantic specifications in logic
- Index-stratified types
- A focused linear logical framework and its application to metatheory of object logics
- Hypothetical reasoning and definitional reflection in logic programming
- Higher-order representation of substructural logics
- Mechanized meta-reasoning using a hybrid HOAS/de Bruijn representation and reflection
- Reasoning with higher-order abstract syntax and contexts: a comparison
- Towards substructural property-based testing
- Nominal abstraction
- A type theory for defining logics and proofs
- Mechanized metatheory revisited: an extended abstract (invited paper)
- A sequent calculus perspective on base-extension semantics
- Facilitating meta-theory reasoning (invited paper)
- Nominal equational narrowing: rewriting for unification in languages with binders
- Types, Tableaus and Gödel’s God in Isabelle/HOL
This page was built for publication: Reasoning with higher-order abstract syntax in a logical framework
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5738952)
