FreshML: programming with binders made simple

DOI10.1145/944705.944729zbMATH1315.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

zbMATH Keywords

variable bindingalpha-conversionmetaprogramming

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Recommendations

• scientific article; zbMATH DE number 1612495
• Generative Unbinding of Names
• Generative unbinding of names
• Binders unbound
• A fresh look at programming with names and binders

Cited in

(42)

• The First-Order Nominal Link
• A general mathematics of names
• A polynomial nominal unification algorithm
• Structural recursion with locally scoped names
• Nominal rewriting
• The locally nameless representation
• Romeo: a system for more flexible binding-safe programming
• Nominal equational logic
• Rule formats for nominal process calculi
• Nominal syntax with atom substitutions
• A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
• Generative unbinding of names
• Abstract syntax: substitution and binders
• A fresh look at programming with names and binders
• A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols
• Romeo: a system for more flexible binding-safe programming
• Denotational semantics with nominal Scott domains
• Incremental rebinding with name polymorphism
• Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus
• Matching and alpha-equivalence check for nominal terms
• Hard life with weak binders
• Binders unbound
• An initial algebra approach to term rewriting systems with variable binders
• Encoding abstract syntax without fresh names
• Programs using syntax with first-class binders
• Free-algebra models for the \(\pi \)-calculus
• On a monadic semantics for freshness
• Nominal unification
• Denotational aspects of untyped normalization by evaluation
• Binding operators for nominal sets
• A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols
• Structuring operational semantics: simplification and computation
• Constrained polymorphic types for a calculus with name variables
• Generative Unbinding of Names
• Programming with binders and indexed data-types
• A dependent type theory with abstractable names
• Nominal Matching and Alpha-Equivalence
• Relating state-based and process-based concurrency through linear logic (full-version)
• Validating Brouwer's continuity principle for numbers using named exceptions
• Nominal AC-matching
• Constraint handling rules with binders, patterns and generic quantification
• Principal types for nominal theories

Describes a project that uses

Uses Software

• FreshML

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)