Enriching an Effect Calculus with Linear Types

DOI10.1007/978-3-642-04027-6_19zbMATH Open1257.03053OpenAlexW1626042158MaRDI QIDQ3644752FDOQ3644752

Authors: J. M. Egger, Rasmus Ejlers Møgelberg, Alex Simpson 

Publication date: 12 November 2009

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

Full work available at URL: https://www.pure.ed.ac.uk/ws/files/12289081/enriched_effect_calculus.pdf

Recommendations

• The enriched effect calculus: syntax and semantics
• Linearly-Used Continuations in the Enriched Effect Calculus
• Linear-use CPS translations in the enriched effect calculus
• The best of both worlds: linear functional programming without compromise
• Linear usage of state

Mathematics Subject Classification ID

Logic in computer science (03B70) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Categorical semantics of formal languages (18C50)

Cites Work

• Title not available (Why is that?)
• From Algol to polymorphic linear lambda-calculus
• Linear logic
• Notions of computation and monads
• Title not available (Why is that?)
• A new constructive logic: classic logic
• Title not available (Why is that?)
• Linear continuation-passing
• Title not available (Why is that?)
• Title not available (Why is that?)
• Linearly-Used Continuations in the Enriched Effect Calculus

Cited In (20)

• ν-Types for Effects and Freshness Analysis
• A theory of effects and resources: adjunction models and polarised calculi
• Computation by interaction for space-bounded functional programming
• On reduction and normalization in the computational core
• A variable typed logic of effects
• Effekt: Capability-passing style for type- and effect-safe, extensible effect handlers in Scala
• Reverse AD at higher types: pure, principled and denotationally correct
• Title not available (Why is that?)
• Linearly-used state in models of call-by-value
• A nominal relational model for local store
• Linearly-Used Continuations in the Enriched Effect Calculus
• Integrating linear and dependent types
• The enriched effect calculus: syntax and semantics
• Linear usage of state
• Enriching a linear/non-linear lambda calculus: a programming language for string diagrams
• Type directed compilation of row-typed algebraic effects
• The best of both worlds: linear functional programming without compromise
• A core quantitative coeffect calculus
• Linear-use CPS translations in the enriched effect calculus
• Title not available (Why is that?)

This page was built for publication: Enriching an Effect Calculus with Linear Types

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3644752)