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

• A new constructive logic: classic logic
• From Algol to polymorphic linear lambda-calculus
• 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?)
• Linear continuation-passing
• Linear logic
• Linearly-Used Continuations in the Enriched Effect Calculus
• Notions of computation and monads

Cited in

(23)

• A variable typed logic of effects
• Reverse AD at higher types: pure, principled and denotationally correct
• Computation by interaction for space-bounded functional programming
• Integrating linear and dependent types
• A theory of effects and resources: adjunction models and polarised calculi
• The enriched effect calculus: syntax and semantics
• The best of both worlds: linear functional programming without compromise
• Linearly-used state in models of call-by-value
• Linear-use CPS translations in the enriched effect calculus
• A nominal relational model for local store
• ν-Types for Effects and Freshness Analysis
• Linearly-Used Continuations in the Enriched Effect Calculus
• scientific article; zbMATH DE number 1942458 (Why is no real title available?)
• LNL-FPC: the linear/non-linear fixpoint calculus
• Effekt: Capability-passing style for type- and effect-safe, extensible effect handlers in Scala
• Enriching a linear/non-linear lambda calculus: a programming language for string diagrams
• Type directed compilation of row-typed algebraic effects
• Linear usage of state
• A core quantitative coeffect calculus
• On reduction and normalization in the computational core
• scientific article; zbMATH DE number 7779295 (Why is no real title available?)
• Amortized analysis via coalgebra
• \(\mathscr{V}\)-graded categories and \(\mathscr{V}\)-\(\mathscr{W}\)-bigraded categories: functor categories and bifunctors over non-symmetric bases

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)