Pages that link to "Item:Q699761"
From MaRDI portal
The following pages link to A new approach to abstract syntax with variable binding (Q699761):
Displaying 50 items.
- Nominal lambda calculus: an internal language for FM-Cartesian closed categories (Q265798) (← links)
- Declarative event based models of concurrency and refinement in psi-calculi (Q272301) (← links)
- A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle (Q286772) (← links)
- Model checking Petri nets with names using data-centric dynamic systems (Q315291) (← links)
- Nominal monoids (Q372971) (← links)
- Full abstraction for Reduced ML (Q388212) (← links)
- Unity in nominal equational reasoning: the algebra of equality on nominal sets (Q420858) (← links)
- Alpha equivalence equalities (Q428860) (← 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)
- Program equivalence in a simple language with state (Q456473) (← links)
- Programming with algebraic effects and handlers (Q478396) (← links)
- Regular and context-free nominal traces (Q530218) (← links)
- Equivariant unification (Q616849) (← links)
- Symmetries, local names and dynamic (de)-allocation of names (Q618165) (← 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)
- Viewing \({\lambda}\)-terms through maps (Q740485) (← links)
- About permutation algebras, (pre)sheaves and named sets (Q853745) (← links)
- A coalgebraic approach to the semantics of the ambient calculus (Q860882) (← links)
- Mechanizing type environments in weak HOAS (Q897934) (← links)
- Nominal techniques in Isabelle/HOL (Q928672) (← links)
- Capture-avoiding substitution as a nominal algebra (Q939160) (← links)
- Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms (Q964000) (← links)
- External and internal syntax of the \(\lambda \)-calculus (Q968531) (← links)
- Matching and alpha-equivalence check for nominal terms (Q980937) (← links)
- A spatial equational logic for the applied \(\pi \)-calculus (Q992517) (← links)
- A study of substitution, using nominal techniques and Fraenkel-Mostowksi sets (Q1006642) (← links)
- HasCasl: integrated higher-order specification and program development (Q1006648) (← links)
- A congruence rule format for name-passing process calculi (Q1012125) (← links)
- Bialgebraic methods and modal logic in structural operational semantics (Q1012126) (← links)
- On the construction of free algebras for equational systems (Q1014644) (← links)
- The lambda-context calculus (extended version) (Q1044184) (← links)
- A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names. (Q1401936) (← links)
- Algorithmic games for full ground references (Q1650867) (← links)
- Simple and subdirectly irreducible finitely supported \(Cb\)-sets (Q1680555) (← links)
- Distinguishing between communicating transactions (Q1706141) (← links)
- Binding operators for nominal sets (Q1744371) (← 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)
- Secrecy and group creation (Q1763430) (← links)
- Fuzzy sets within finitely supported mathematics (Q1794962) (← links)
- Free functor from the category of \(G\)-nominal sets to that of 01-\(G\)-nominal sets (Q1797955) (← links)
- Nominal unification (Q1882909) (← links)
- Nominal logic, a first order theory of names and binding (Q1887151) (← links)
- A spatial logic for concurrency. I (Q1887152) (← links)
- Nested abstract syntax in Coq (Q1945918) (← links)
- A formalized general theory of syntax with bindings: extended version (Q1984791) (← links)
- Permutation groups with small orbit growth (Q2037519) (← links)
- Confluence and commutation for nominal rewriting systems with atom-variables (Q2119102) (← links)
