Nominal logic, a first order theory of names and binding
From MaRDI portal
Publication:1887151
DOI10.1016/S0890-5401(03)00138-XzbMATH Open1056.03014WikidataQ29393340 ScholiaQ29393340MaRDI QIDQ1887151FDOQ1887151
Publication date: 23 November 2004
Published in: Information and Computation (Search for Journal in Brave)
Recommendations
Variable bindingAbstract syntaxpermutation modelfirst-order many-sorted logicFresh namesname-swapping
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) Semantics in the theory of computing (68Q55)
Cites Work
- Isabelle. A generic theorem prover
- Some lambda calculus and type theory formalized
- Title not available (Why is that?)
- Title not available (Why is that?)
- Endliche Gruppen I
- A new approach to abstract syntax with variable binding
- The lambda calculus. Its syntax and semantics. Rev. ed.
- First order categorical logic. Model-theoretical methods in the theory of topoi and related categories
- Title not available (Why is that?)
- Reasoning with higher-order abstract syntax in a logical framework
- A compact representation of proofs
- Title not available (Why is that?)
- Partial inductive definitions
- The axiom of choice
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- An application of open maps to categorical logic
- HOL-\(\lambda\sigma\): An intentional first-order expression of higher-order logic
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Elementary structures in process theory (1): Sets with renaming
- Title not available (Why is that?)
- Developing (meta)theory of \(\lambda\)-calculus in the theory of contexts
Cited In (only showing first 100 items - show all)
- Title not available (Why is that?)
- Abstract Syntax: Substitution and Binders
- A dependent type theory with abstractable names
- Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus
- Nominal lambda calculus: an internal language for FM-Cartesian closed categories
- A linear logic framework for multimodal logics
- Alpha equivalence equalities
- Viewing \({\lambda}\)-terms through maps
- Matching and alpha-equivalence check for nominal terms
- Mechanized metatheory revisited
- Alpha-structural induction and recursion for the lambda calculus in constructive type theory
- A congruence rule format for name-passing process calculi
- An initial algebra approach to term rewriting systems with variable binders
- Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations
- Nominal Unification from a Higher-Order Perspective
- PNL to HOL: from the logic of nominal sets to the logic of higher-order functions
- Title not available (Why is that?)
- Programs Using Syntax with First-Class Binders
- Incorporating quotation and evaluation into Church's type theory
- A polynomial nominal unification algorithm
- ASP\(_{\text{fun}}\) : a typed functional active object calculus
- A study of substitution, using nominal techniques and Fraenkel-Mostowksi sets
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- Unranked Nominal Unification
- Nominal abstraction
- Psi-calculi in Isabelle
- Computing strong and weak bisimulations for psi-calculi
- Nominal essential intersection types
- A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols
- Title not available (Why is that?)
- A canonical locally named representation of binding
- Nominal unification
- External and internal syntax of the \(\lambda \)-calculus
- Equivariant unification
- Regular behaviours with names: on rational fixpoints of endofunctors on nominal sets
- The First-Order Nominal Link
- Fixed-Point Constraints for Nominal Equational Unification
- Logic Programming
- Higher-order psi-calculi
- Mechanizing type environments in weak HOAS
- Free-algebra models for the \(\pi \)-calculus
- A simple nominal type theory
- Nominal rewriting
- About permutation algebras, (pre)sheaves and named sets
- Free functor from the category of \(G\)-nominal sets to that of 01-\(G\)-nominal sets
- Nominal equational logic
- Satisfiability in composition-nominative logics
- A general mathematics of names
- Foundations of Nominal Techniques: Logic and Semantics of Variables in Abstract Syntax
- General Bindings and Alpha-Equivalence in Nominal Isabelle
- Structural recursion with locally scoped names
- Simple and subdirectly irreducible finitely supported \(Cb\)-sets
- A Sorted Semantic Framework for Applied Process Calculi (Extended Abstract)
- Psi-calculi in Isabelle
- A solution to the PoplMark challenge based on de Bruijn indices
- Formal metatheory of programming languages in the Matita interactive theorem prover
- Nominal techniques in Isabelle/HOL
- Finite and infinite support in nominal algebra and logic: nominal completeness theorems for free
- A two-level logic approach to reasoning about computations
- Broadcast Psi-calculi with an Application to Wireless Protocols
- A Compiled Implementation of Normalization by Evaluation
- Two-level nominal sets and semantic nominal terms: an extension of nominal set theory for handling meta-variables
- Nominal Matching and Alpha-Equivalence
- Distinguishing between communicating transactions
- Fresh logic: Proof-theory and semantics for FM and nominal techniques
- OMFM: A framework of object merging based on fuzzy multisets
- Rensets and renaming-based recursion for syntax with bindings
- A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs
- Confluence and commutation for nominal rewriting systems with atom-variables
- Machine-checked proof of the Church-Rosser theorem for the lambda calculus using the Barendregt variable convention in constructive type theory
- Formal metatheory of the lambda calculus using Stoughton's substitution
- a-Logic With Arrows
- Nominal SOS
- Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem
- Title not available (Why is that?)
- Modules over relative monads for syntax and semantics
- Implementing Spi Calculus Using Nominal Techniques
- Mechanizing metatheory without typing contexts
- Nominal Confluence Tool
- \(\mathrm{HO}\pi\) in Coq
- Ugo Montanari and Software Verification
- A program logic for fresh name generation
- Reductive logic, proof-search, and coalgebra: a perspective from resource semantics
- Matching logic explained
- On the role of names in reasoning about \(\lambda\)-tree syntax specifications
- On a monadic semantics for freshness
- Nominal syntax with atom substitutions
- The nominal/FM Yoneda Lemma
- An extension of a permutative model of set theory
- Formal SOS-Proofs for the Lambda-Calculus
- Formal Reasoning Using Distributed Assertions
- Title not available (Why is that?)
- Ground confluence and strong commutation modulo alpha-equivalence in nominal rewriting
- Rensets and renaming-based recursion for syntax with bindings extended version
- Constructing weak simulations from linear implications for processes with private names
- Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention
- Nominal Inversion Principles
- Undecidability of model checking in brane logic
- Title not available (Why is that?)
- A Survey of the Proof-Theoretic Foundations of Logic Programming
Uses Software
This page was built for publication: Nominal logic, a first order theory of names and binding
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1887151)
