Pages that link to "Item:Q1887151"
From MaRDI portal
The following pages link to Nominal logic, a first order theory of names and binding (Q1887151):
Displaying 50 items.
- Nominal lambda calculus: an internal language for FM-Cartesian closed categories (Q265798) (← links)
- Regular behaviours with names: on rational fixpoints of endofunctors on nominal sets (Q328657) (← links)
- Alpha equivalence equalities (Q428860) (← links)
- ASP\(_{\text{fun}}\) : a typed functional active object calculus (Q433340) (← links)
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (Q438569) (← links)
- Computing strong and weak bisimulations for psi-calculi (Q444457) (← 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)
- Nominal abstraction (Q617715) (← links)
- PNL to HOL: from the logic of nominal sets to the logic of higher-order functions (Q714797) (← links)
- Viewing \({\lambda}\)-terms through maps (Q740485) (← links)
- Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations (Q853738) (← links)
- An initial algebra approach to term rewriting systems with variable binders (Q853743) (← links)
- About permutation algebras, (pre)sheaves and named sets (Q853745) (← links)
- Mechanizing type environments in weak HOAS (Q897934) (← links)
- Nominal techniques in Isabelle/HOL (Q928672) (← links)
- A polynomial nominal unification algorithm (Q944382) (← links)
- External and internal syntax of the \(\lambda \)-calculus (Q968531) (← links)
- Matching and alpha-equivalence check for nominal terms (Q980937) (← links)
- A study of substitution, using nominal techniques and Fraenkel-Mostowksi sets (Q1006642) (← links)
- A congruence rule format for name-passing process calculi (Q1012125) (← links)
- Nominal essential intersection types (Q1643145) (← links)
- Simple and subdirectly irreducible finitely supported \(Cb\)-sets (Q1680555) (← links)
- Distinguishing between communicating transactions (Q1706141) (← links)
- OMFM: A framework of object merging based on fuzzy multisets (Q1718080) (← links)
- Alpha-structural induction and recursion for the lambda calculus in constructive type theory (Q1744410) (← links)
- Incorporating quotation and evaluation into Church's type theory (Q1753993) (← links)
- Free functor from the category of \(G\)-nominal sets to that of 01-\(G\)-nominal sets (Q1797955) (← links)
- Nominal unification (Q1882909) (← links)
- A solution to the PoplMark challenge based on de Bruijn indices (Q1945917) (← links)
- Formal metatheory of programming languages in the Matita interactive theorem prover (Q1945919) (← links)
- \(\mathrm{HO}\pi\) in Coq (Q2031410) (← links)
- Matching logic explained (Q2035650) (← links)
- Rensets and renaming-based recursion for syntax with bindings (Q2104549) (← links)
- Confluence and commutation for nominal rewriting systems with atom-variables (Q2119102) (← links)
- A program logic for fresh name generation (Q2145263) (← links)
- Mechanized metatheory revisited (Q2323447) (← links)
- Machine-checked proof of the Church-Rosser theorem for the lambda calculus using the Barendregt variable convention in constructive type theory (Q2333314) (← links)
- Mechanizing metatheory without typing contexts (Q2352491) (← links)
- Formal metatheory of the lambda calculus using Stoughton's substitution (Q2358702) (← links)
- Fresh logic: Proof-theory and semantics for FM and nominal techniques (Q2372191) (← links)
- Nominal rewriting (Q2373703) (← links)
- A general mathematics of names (Q2373874) (← links)
- A canonical locally named representation of binding (Q2392482) (← links)
- A two-level logic approach to reasoning about computations (Q2392484) (← links)
- A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols (Q2424886) (← links)
- Satisfiability in composition-nominative logics (Q2445092) (← links)
- Free-algebra models for the \(\pi \)-calculus (Q2474057) (← links)
- On a monadic semantics for freshness (Q2566026) (← links)
