Nominal abstraction

DOI10.1016/j.ic.2010.09.004zbMath1215.03049OpenAlexW2912466821MaRDI QIDQ617715

Gopalan Nadathur, Andrew Gacek, Dale A. Miller

Publication date: 13 January 2011

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2010.09.004

zbMATH Keywords

proof searchhigher-order abstract syntax\(\lambda \)-tree syntaxgeneric judgmentsreasoning about operational semantics

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey, The undecidability of proof search when equality is a logical connective, A two-level logic approach to reasoning about computations, A Survey of the Proof-Theoretic Foundations of Logic Programming, Formalized meta-theory of sequent calculi for linear logics, Cut elimination for a logic with induction and co-induction, Formalized meta-theory of sequent calculi for substructural logics, Proof Pearl: Abella Formalization of λ-Calculus Cube Property, Unnamed Item, Constructing weak simulations from linear implications for processes with private names, Mechanized metatheory revisited

Uses Software

• Twelf
• Bedwyr
• Abella
• Nominal Isabelle
• Centaur

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Equivariant unification
• Nominal techniques in Isabelle/HOL
• Unification under a mixed prefix
• A unification algorithm for typed \(\overline\lambda\)-calculus
• Encoding transition systems in sequent calculus
• Cut-elimination for a logic with definitions and induction
• Nominal logic, a first order theory of names and binding
• Fresh logic: Proof-theory and semantics for FM and nominal techniques
• Uniform proofs as a foundation for logic programming
• On the Expressivity of Minimal Generic Quantification
• Reasoning in Abella about Structural Operational Semantics Specifications
• Proof search specifications of bisimulation and modal logics for the π-calculus
• The Abella Interactive Theorem Prover (System Description)
• Alpha-structural recursion and induction
• A framework for defining logics
• A proof theory for generic judgments
• Intensional interpretations of functionals of finite type I
• Foundations of Software Science and Computational Structures
• Types for Proofs and Programs
• Reasoning with higher-order abstract syntax in a logical framework