Nominal logic, a first order theory of names and binding

DOI10.1016/S0890-5401(03)00138-XzbMath1056.03014WikidataQ29393340 ScholiaQ29393340MaRDI QIDQ1887151

Andrew M. Pitts

Publication date: 23 November 2004

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

zbMATH Keywords

Variable bindingAbstract syntaxpermutation modelfirst-order many-sorted logicFresh namesname-swapping

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Nominal lambda calculus: an internal language for FM-Cartesian closed categories, Formal metatheory of the lambda calculus using Stoughton's substitution, A linear logic framework for multimodal logics, Nominal unification, Fresh logic: Proof-theory and semantics for FM and nominal techniques, Nominal rewriting, A general mathematics of names, Nominal SOS, A program logic for fresh name generation, Nominal essential intersection types, Regular behaviours with names: on rational fixpoints of endofunctors on nominal sets, Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations, An initial algebra approach to term rewriting systems with variable binders, About permutation algebras, (pre)sheaves and named sets, Finite and infinite support in nominal algebra and logic: nominal completeness theorems for free, Unnamed Item, An Extension of a Permutative Model of Set Theory, A canonical locally named representation of binding, A two-level logic approach to reasoning about computations, Nominal syntax with atom substitutions, Unnamed Item, Simple and subdirectly irreducible finitely supported \(Cb\)-sets, Equivariant unification, Nominal abstraction, A Survey of the Proof-Theoretic Foundations of Logic Programming, Ground confluence and strong commutation modulo alpha-equivalence in nominal rewriting, Rensets and renaming-based recursion for syntax with bindings extended version, Mechanizing type environments in weak HOAS, Ugo Montanari and Software Verification, Implementing Spi Calculus Using Nominal Techniques, A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols, Nominal Matching and Alpha-Equivalence, A solution to the PoplMark challenge based on de Bruijn indices, Formal metatheory of programming languages in the Matita interactive theorem prover, Alpha equivalence equalities, ASP\(_{\text{fun}}\) : a typed functional active object calculus, Distinguishing between communicating transactions, Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax, Computing strong and weak bisimulations for psi-calculi, Psi-calculi in Isabelle, Satisfiability in composition-nominative logics, OMFM: A framework of object merging based on fuzzy multisets, Psi-calculi in Isabelle, Programs Using Syntax with First-Class Binders, Nominal techniques in Isabelle/HOL, Fixed-Point Constraints for Nominal Equational Unification, A Compiled Implementation of Normalization by Evaluation, Nominal Inversion Principles, The First-Order Nominal Link, A polynomial nominal unification algorithm, a-Logic With Arrows, Alpha-structural induction and recursion for the lambda calculus in constructive type theory, Foundations of Nominal Techniques: Logic and Semantics of Variables in Abstract Syntax, Structural recursion with locally scoped names, Free-algebra models for the \(\pi \)-calculus, Incorporating quotation and evaluation into Church's type theory, A dependent type theory with abstractable names, Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus, External and internal syntax of the \(\lambda \)-calculus, Higher-order psi-calculi, Modules over relative monads for syntax and semantics, Formal SOS-Proofs for the Lambda-Calculus, Matching and alpha-equivalence check for nominal terms, PNL to HOL: from the logic of nominal sets to the logic of higher-order functions, Unnamed Item, \(\mathrm{HO}\pi\) in Coq, Matching logic explained, A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs, Free functor from the category of \(G\)-nominal sets to that of 01-\(G\)-nominal sets, A Simple Nominal Type Theory, On the Role of Names in Reasoning about λ-tree Syntax Specifications, General Bindings and Alpha-Equivalence in Nominal Isabelle, Nominal Unification from a Higher-Order Perspective, A study of substitution, using nominal techniques and Fraenkel-Mostowksi sets, Viewing \({\lambda}\)-terms through maps, A congruence rule format for name-passing process calculi, Nominal Confluence Tool, Two-level nominal sets and semantic nominal terms: an extension of nominal set theory for handling meta-variables, Broadcast Psi-calculi with an Application to Wireless Protocols, A Sorted Semantic Framework for Applied Process Calculi (Extended Abstract), Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem, The nominal/FM Yoneda Lemma, Constructing weak simulations from linear implications for processes with private names, Mechanized metatheory revisited, On a monadic semantics for freshness, Machine-checked proof of the Church-Rosser theorem for the lambda calculus using the Barendregt variable convention in constructive type theory, Nominal Equational Logic, Undecidability of Model Checking in Brane Logic, Rensets and renaming-based recursion for syntax with bindings, Abstract Syntax: Substitution and Binders, Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention, Mechanizing metatheory without typing contexts, Contextual equivalence for inductive definitions with binders in higher order typed functional programming, Confluence and commutation for nominal rewriting systems with atom-variables

Uses Software

• Coq
• Isabelle
• SLMC

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A new approach to abstract syntax with variable binding
• The lambda calculus. Its syntax and semantics. Rev. ed.
• An application of open maps to categorical logic
• A compact representation of proofs
• Partial inductive definitions
• First order categorical logic. Model-theoretical methods in the theory of topoi and related categories
• Isabelle. A generic theorem prover
• Some lambda calculus and type theory formalized
• HOL-λσ: an intentional first-order expression of higher-order logic
• Developing (Meta)Theory of λ-calculus in the Theory of Contexts1 1Work partially supported by Italian MURST project tosca and EC-WG types.
• Elementary structures in process theory (1): Sets with renaming
• Endliche Gruppen I
• Reasoning with higher-order abstract syntax in a logical framework
• The axiom of choice