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