FreshML

DOI10.1145/944705.944729zbMath1315.68058OpenAlexW2136171121MaRDI QIDQ5261281

Mark R. Shinwell, Andrew M. Pitts, Murdoch James 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)

Related Items (35)

Nominal unification ⋮ Nominal rewriting ⋮ A general mathematics of names ⋮ An initial algebra approach to term rewriting systems with variable binders ⋮ Denotational aspects of untyped normalization by evaluation ⋮ Unnamed Item ⋮ Nominal syntax with atom substitutions ⋮ Constraint handling rules with binders, patterns and generic quantification ⋮ Nominal AC-matching ⋮ A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols ⋮ Nominal Matching and Alpha-Equivalence ⋮ The locally nameless representation ⋮ Romeo: A system for more flexible binding-safe programming ⋮ Programs Using Syntax with First-Class Binders ⋮ The First-Order Nominal Link ⋮ Validating Brouwer's continuity principle for numbers using named exceptions ⋮ A polynomial nominal unification algorithm ⋮ Binding operators for nominal sets ⋮ A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols ⋮ Structural recursion with locally scoped names ⋮ Free-algebra models for the \(\pi \)-calculus ⋮ A dependent type theory with abstractable names ⋮ Proof-Relevant Logical Relations for Name Generation ⋮ Hard Life with Weak Binders ⋮ Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus ⋮ Matching and alpha-equivalence check for nominal terms ⋮ Relating state-based and process-based concurrency through linear logic (full-version) ⋮ Incremental rebinding with name polymorphism ⋮ Unnamed Item ⋮ Principal Types for Nominal Theories ⋮ On a monadic semantics for freshness ⋮ Denotational Semantics with Nominal Scott Domains ⋮ Nominal Equational Logic ⋮ Structuring Operational Semantics: Simplification and Computation ⋮ Abstract Syntax: Substitution and Binders

Uses Software

• Freshml

This page was built for publication: FreshML