Nominal unification
From MaRDI portal
Publication:1882909
DOI10.1016/j.tcs.2004.06.016zbMath1078.68140OpenAlexW2912255765MaRDI QIDQ1882909
Christian Urban, Andrew M. Pitts, Murdoch James Gabbay
Publication date: 1 October 2004
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2004.06.016
Related Items
Declarative event based models of concurrency and refinement in psi-calculi, Nominal rewriting, Nominal SOS, From natural semantics to C: A formal derivation of two STG machines, Nominal essential intersection types, Finite and infinite support in nominal algebra and logic: nominal completeness theorems for free, Encoding abstract syntax without fresh names, Nominal Unification and Matching of Higher Order Expressions with Recursive Let, Unnamed Item, A unified rule format for bounded nondeterminism in SOS with terms as labels, Nominal syntax with atom substitutions, A Certified Functional Nominal C-Unification Algorithm, Declarative Compilation for Constraint Logic Programming, Equivariant unification, αCheck: A mechanized metatheory model checker, Ground confluence and strong commutation modulo alpha-equivalence in nominal rewriting, A Formal Proof of the Strong Normalization Theorem for System T in Agda, Nominal AC-matching, A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols, Unity in nominal equational reasoning: the algebra of equality on nominal sets, Nominal Matching and Alpha-Equivalence, Alpha equivalence equalities, On solving nominal disunification constraints, Nominal techniques in Isabelle/HOL, Fixed-Point Constraints for Nominal Equational Unification, Rewriting with generalized nominal unification, Capture-avoiding substitution as a nominal algebra, Nominal equational problems, The First-Order Nominal Link, What Is Essential Unification?, Imaginary groups: lazy monoids and reversible computation, A polynomial nominal unification algorithm, Checking overlaps of nominal rewriting rules, Completeness in PVS of a nominal unification algorithm, A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols, Constraint logic programming with a relational machine, Structural recursion with locally scoped names, A dependent type theory with abstractable names, Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus, Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms, Matching and alpha-equivalence check for nominal terms, PNL to HOL: from the logic of nominal sets to the logic of higher-order functions, Representation and duality of the untyped \(\lambda\)-calculus in nominal lattice and topological semantics, with a proof of topological completeness, HM(X) type inference is CLP(X) solving, A Simple Nominal Type Theory, Nominal Unification from a Higher-Order Perspective, A study of substitution, using nominal techniques and Fraenkel-Mostowksi sets, Nominal Confluence Tool, Principal Types for Nominal Theories, Two-level nominal sets and semantic nominal terms: an extension of nominal set theory for handling meta-variables, Two-level Lambda-calculus, SUBSEXPL: a tool for simulating and comparing explicit substitutions calculi ★, The lambda-context calculus (extended version), Coverability Synthesis in Parametric Petri Nets, α lean TA P: A Declarative Theorem Prover for First-Order Classical Logic, A formalisation of nominal C-matching through unification with protected variables, Nominal Equational Logic, Implementing Nominal Unification, Formalising nominal C-unification generalised with protected variables, Contextual equivalence for inductive definitions with binders in higher order typed functional programming, Confluence and commutation for nominal rewriting systems with atom-variables, \texttt{slepice}: towards a verified implementation of type theory in type theory
Uses Software
Cites Work
- 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.
- A calculus of mobile processes. II
- Linear unification
- The Qu-Prolog unification algorithm: formalisation and correctness
- On the algebraic models of lambda calculus
- Higher order unification via explicit substitutions
- Nominal logic, a first order theory of names and binding
- An Efficient Unification Algorithm
- A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
- Unification of higher-order patterns in linear time and space
- FreshML
- Computer Science Logic
- Computer Science Logic
- A typed context calculus
