Enriching an Effect Calculus with Linear Types

DOI10.1007/978-3-642-04027-6_19MaRDI QIDQ3644752zbMATH OpenOpenAlexFDO

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

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)

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

Cites work

• scientific article; zbMATH DE number 4179333 (Why is no real title available?)
• scientific article; zbMATH DE number 3751225 (Why is no real title available?)
• scientific article; zbMATH DE number 1942458 (Why is no real title available?)
• scientific article; zbMATH DE number 2079022 (Why is no real title available?)
• scientific article; zbMATH DE number 2172969 (Why is no real title available?)
• A new constructive logic: classic logic
• From Algol to polymorphic linear lambda-calculus
• Linear continuation-passing
• Linear logic
• Linearly-Used Continuations in the Enriched Effect Calculus
• Notions of computation and monads

Cited in

(20)

• scientific article; zbMATH DE number 1942458 (Why is no real title available?)
• ν-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
• A variable typed logic of effects
• On reduction and normalization in the computational core
• Effekt: Capability-passing style for type- and effect-safe, extensible effect handlers in Scala
• Reverse AD at higher types: pure, principled and denotationally correct
• scientific article; zbMATH DE number 7779295 (Why is no real title available?)
• 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

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)