Cited in
(68)- Programs using syntax with first-class binders
- A dependent type theory with abstractable names
- Denotational semantics with nominal Scott domains
- Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus
- Matching and alpha-equivalence check for nominal terms
- Binding operators for nominal sets
- A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols
- Mechanized metatheory revisited
- Formal Methods for Components and Objects
- An initial algebra approach to term rewriting systems with variable binders
- Generalised name abstraction for nominal sets
- A universe of binding and computation
- A polynomial nominal unification algorithm
- Constrained polymorphic types for a calculus with name variables
- On nominal regular languages with binders
- FreshML: programming with binders made simple
- The locally nameless representation
- Foundations of nominal techniques: logic and semantics of variables in abstract syntax
- A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols
- Incremental rebinding with name polymorphism
- Principal types for nominal theories
- Refined environment classifiers. Type- and scope-safe code generation with mutable cells
- Nominal unification
- Structuring operational semantics: simplification and computation
- Ott
- Beluga
- SafeDpi
- TinkerType
- VESTA
- TAMPR
- SLMC
- OCaml
- Pict
- BER MetaOCaml
- ULM
- aleanTAP
- MoMo
- Gmeta
- Nominal Isabelle
- RepLib
- Qu-Prolog
- Delphin
- FreshOCaml
- HNT
- Unbound
- Rule formats for nominal process calculi
- The First-Order Nominal Link
- Relating state-based and process-based concurrency through linear logic (full-version)
- Logic Programming
- Hard life with weak binders
- Nominal syntax with atom substitutions
- Ott: Effective tool support for the working semanticist
- Free-algebra models for the \(\pi \)-calculus
- A simple nominal type theory
- Binders unbound
- Nominal rewriting
- Foundations of Software Science and Computation Structures
- Nominal equational logic
- Validating Brouwer's continuity principle for numbers using named exceptions
- A dependent nominal type theory
- A general mathematics of names
- Structural recursion with locally scoped names
- Program transformation with scoped dynamic rewrite rules
- Acute: High-level programming language design for distributed computation
- Denotational aspects of untyped normalization by evaluation
- A fresh look at programming with names and binders
- Programming type-safe transformations using higher-order abstract syntax
- Freshness and Name-Restriction in Sets of Traces with Names
This page was built for software: FreshML
