On a monadic semantics for freshness

DOI10.1016/j.tcs.2005.06.003zbMath1077.68050OpenAlexW2128159126MaRDI QIDQ2566026

Andrew M. Pitts, Mark R. Shinwell

Publication date: 22 September 2005

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2005.06.003

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55)

Related Items

A general mathematics of names, A Nominal Relational Model for Local Store, Encoding abstract syntax without fresh names, On Normalization by Evaluation for Object Calculi, Deciding contextual equivalence of \(\nu \)-calculus with effectful contexts, Interpreting Localized Computational Effects Using Operators of Higher Type, a-Logic With Arrows, Foundations of Nominal Techniques: Logic and Semantics of Variables in Abstract Syntax, Free-algebra models for the \(\pi \)-calculus, Proof-Relevant Logical Relations for Name Generation, Cryptographic logical relations, Hard Life with Weak Binders, Denotational Semantics with Nominal Scott Domains, Sequentiality and the CPS Semantics of Fresh Names, Contextual equivalence for inductive definitions with binders in higher order typed functional programming

Uses Software

• OCaml

Cites Work

• A new approach to abstract syntax with variable binding
• Notions of computation and monads
• The lambda calculus. Its syntax and semantics. Rev. ed.
• LCF considered as a programming language
• A syntactic approach to type soundness
• Nominal logic, a first order theory of names and binding
• Relational properties of domains
• Comprehending monads
• Equivalence in functional languages with effects
• FreshML
• Computer Science Logic
• Unnamed Item
• Unnamed Item
• Unnamed Item