FreshML: programming with binders made simple
From MaRDI portal
(Redirected from Publication:5261281)
Recommendations
Cited in
(46)- Binding operators for nominal sets
- A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols
- Nominal unification
- The locally nameless representation
- Nominal rewriting
- A general mathematics of names
- Encoding abstract syntax without fresh names
- A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols
- Free-algebra models for the \(\pi \)-calculus
- On a monadic semantics for freshness
- Nominal syntax with atom substitutions
- Romeo: a system for more flexible binding-safe programming
- Nominal equational logic
- Structuring operational semantics: simplification and computation
- Programming with binders and indexed data-types
- Programs using syntax with first-class binders
- The First-Order Nominal Link
- Structural recursion with locally scoped names
- Principal types for nominal theories
- Generative unbinding of names
- Nominal Matching and Alpha-Equivalence
- Generative Unbinding of Names
- Constrained polymorphic types for a calculus with name variables
- Constraint handling rules with binders, patterns and generic quantification
- Validating Brouwer's continuity principle for numbers using named exceptions
- Rule formats for nominal process calculi
- A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
- Hard life with weak binders
- A fresh look at programming with names and binders
- Binders unbound
- Abstract syntax: substitution and binders
- A dependent type theory with abstractable names
- Denotational aspects of untyped normalization by evaluation
- Romeo: a system for more flexible binding-safe programming
- Denotational semantics with nominal Scott domains
- Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus
- Nominal AC-matching
- Strong nominal semantics for fixed-point constraints
- Nominal Henkin semantics: simply-typed lambda-calculus models in nominal sets
- Abstract representation of binders in OCaml using the Bindlib library
- Formalisation in constructive type theory of Barendregt's variable convention for generic structures with binders
- Relating state-based and process-based concurrency through linear logic (full-version)
- Incremental rebinding with name polymorphism
- An initial algebra approach to term rewriting systems with variable binders
- A polynomial nominal unification algorithm
- Matching and alpha-equivalence check for nominal terms
This page was built for publication: FreshML: programming with binders made simple
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5261281)
