FreshML: programming with binders made simple
From MaRDI portal
Publication:5261281
DOI10.1145/944705.944729zbMATH Open1315.68058OpenAlexW2136171121MaRDI QIDQ5261281FDOQ5261281
Authors: Mark R. Shinwell, Andrew M. Pitts, Murdoch J. Gabbay 
Publication date: 2 July 2015
Published in: Proceedings of the eighth ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/944705.944729
Recommendations
Cited In (43)
- Generative Unbinding of Names
- 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
- An initial algebra approach to term rewriting systems with variable binders
- Proof-relevant logical relations for name generation
- Constrained polymorphic types for a calculus with name variables
- A polynomial nominal unification algorithm
- The locally nameless representation
- Abstract syntax: substitution and binders
- A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols
- Principal types for nominal theories
- Incremental rebinding with name polymorphism
- Romeo: a system for more flexible binding-safe programming
- Nominal unification
- Structuring operational semantics: simplification and computation
- Rule formats for nominal process calculi
- The First-Order Nominal Link
- Hard life with weak binders
- On a monadic semantics for freshness
- Relating state-based and process-based concurrency through linear logic (full-version)
- Nominal syntax with atom substitutions
- Romeo: a system for more flexible binding-safe programming
- Free-algebra models for the \(\pi \)-calculus
- Binders unbound
- Nominal rewriting
- Validating Brouwer's continuity principle for numbers using named exceptions
- Nominal equational logic
- Encoding abstract syntax without fresh names
- A general mathematics of names
- Structural recursion with locally scoped names
- Denotational aspects of untyped normalization by evaluation
- Generative unbinding of names
- A fresh look at programming with names and binders
- Nominal Matching and Alpha-Equivalence
- Programming with binders and indexed data-types
- Nominal AC-matching
- Constraint handling rules with binders, patterns and generic quantification
- A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
- Programs using syntax with first-class binders
Uses Software
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)
