Nominal Logic Programming

Abstract

Nominal logic is an extension of first-order logic which provides a simple foundation for formalizing and reasoning about abstract syntax modulo consistent renaming of bound names (that is, alpha-equivalence). This article investigates logic programming based on nominal logic. We describe some typical nominal logic programs, and develop the model-theoretic, proof-theoretic, and operational semantics of such programs. Besides being of interest for ensuring the correct behavior of implementations, these results provide a rigorous foundation for techniques for analysis and reasoning about nominal logic programs, as we illustrate via examples.

46 pages; 19 page appendix; 13 figures. Revised journal submission as of July 23, 2007

References in corpus (2)

• Nominal Logic Programming
• Constraint Logic Programming with Hereditary Harrop Formula

Cited by in corpus (16)

• Nominal Logic Programming
• A Framework for Specifying, Prototyping, and Reasoning about Computational Systems
• Permissive nominal terms and their unification: an infinite, co-infinite approach to nominal techniques
• $\alpha$Check: A mechanized metatheory model-checker
• Nominal Unification of Higher Order Expressions with Recursive Let
• Reasoning About Higher-Order Relational Specifications
• PNL to HOL: from the logic of nominal sets to the logic of higher-order functions
• From nominal sets binding to functions and lambda-abstraction: connecting the logic of permutation models with the logic of functions
• Logic Column 14: Nominal Logic and Abstract Syntax
• Nominal Unification and Matching of Higher Order Expressions with Recursive Let
• Nominal Matching Logic
• Constraint solving in non-permutative nominal abstract syntax
• A simple sequent calculus for nominal logic
• Relating Nominal and Higher-order Abstract Syntax Specifications
• Nominal Abstraction
• On Nominal Syntax and Permutation Fixed Points