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, α-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.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Aug 01, 2008
- Source ID
- 10.1145/1387673.1387675
Entities
People
- Christian Urban
- James Cheney
Organizations
- Air Force Office of Scientific Research
- Engineering and Physical Sciences Research Council
- Office of Naval Research
- Technische Universität Ilmenau
- University of Edinburgh