The following pages link to Nominal unification (Q1882909):
Displaying 50 items.
- Declarative event based models of concurrency and refinement in psi-calculi (Q272301) (← links)
- Unity in nominal equational reasoning: the algebra of equality on nominal sets (Q420858) (← links)
- Alpha equivalence equalities (Q428860) (← links)
- Constraint logic programming with a relational machine (Q511023) (← links)
- A dependent type theory with abstractable names (Q530845) (← links)
- Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus (Q530864) (← links)
- Equivariant unification (Q616849) (← links)
- PNL to HOL: from the logic of nominal sets to the logic of higher-order functions (Q714797) (← links)
- Representation and duality of the untyped \(\lambda\)-calculus in nominal lattice and topological semantics, with a proof of topological completeness (Q730088) (← links)
- Nominal techniques in Isabelle/HOL (Q928672) (← links)
- Capture-avoiding substitution as a nominal algebra (Q939160) (← links)
- A polynomial nominal unification algorithm (Q944382) (← links)
- Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms (Q964000) (← links)
- Matching and alpha-equivalence check for nominal terms (Q980937) (← links)
- A study of substitution, using nominal techniques and Fraenkel-Mostowksi sets (Q1006642) (← links)
- The lambda-context calculus (extended version) (Q1044184) (← links)
- Nominal essential intersection types (Q1643145) (← links)
- Checking overlaps of nominal rewriting rules (Q1744404) (← links)
- Completeness in PVS of a nominal unification algorithm (Q1744405) (← links)
- A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols (Q1744440) (← links)
- Confluence and commutation for nominal rewriting systems with atom-variables (Q2119102) (← links)
- \texttt{slepice}: towards a verified implementation of type theory in type theory (Q2119108) (← links)
- On solving nominal disunification constraints (Q2219072) (← links)
- Nominal equational problems (Q2233392) (← links)
- A formalisation of nominal C-matching through unification with protected variables (Q2333665) (← links)
- Nominal rewriting (Q2373703) (← links)
- Encoding abstract syntax without fresh names (Q2392477) (← links)
- A unified rule format for bounded nondeterminism in SOS with terms as labels (Q2403821) (← links)
- A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols (Q2424886) (← links)
- Nominal syntax with atom substitutions (Q2662669) (← links)
- A Simple Nominal Type Theory (Q2804939) (← links)
- Nominal Confluence Tool (Q2817917) (← links)
- Nominal Equational Logic (Q2864152) (← links)
- Implementing Nominal Unification (Q2867897) (← links)
- Contextual equivalence for inductive definitions with binders in higher order typed functional programming (Q2875221) (← links)
- Finite and infinite support in nominal algebra and logic: nominal completeness theorems for free (Q2915895) (← links)
- Declarative Compilation for Constraint Logic Programming (Q2949715) (← links)
- The First-Order Nominal Link (Q3003496) (← links)
- Structural recursion with locally scoped names (Q3016213) (← links)
- Principal Types for Nominal Theories (Q3088280) (← links)
- Two-level nominal sets and semantic nominal terms: an extension of nominal set theory for handling meta-variables (Q3094165) (← links)
- Nominal SOS (Q3178277) (← links)
- What Is Essential Unification? (Q3305325) (← links)
- Nominal Matching and Alpha-Equivalence (Q3511452) (← links)
- SUBSEXPL: a tool for simulating and comparing explicit substitutions calculi ★ (Q3647258) (← links)
- αCheck: A mechanized metatheory model checker (Q4593089) (← links)
- (Q4972733) (← links)
- Two-level Lambda-calculus (Q4982628) (← links)
- Fixed-Point Constraints for Nominal Equational Unification (Q4993333) (← links)
- Formalising nominal C-unification generalised with protected variables (Q5022930) (← links)
