No value restriction is needed for algebraic effects and handlers
From MaRDI portal
Publication:5372003
DOI10.1017/S0956796816000320zbMath1418.68034arXiv1605.06938MaRDI QIDQ5372003
Publication date: 23 October 2017
Published in: Journal of Functional Programming (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1605.06938
Related Items
Factorisation systems for logical relations and monadic lifting in type-and-effect system semantics ⋮ Local algebraic effect theories ⋮ Continuation passing style for effect handlers
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Normalization by evaluation and algebraic effects
- Programming with algebraic effects and handlers
- Notions of computation and monads
- Type inference for polymorphic references
- On the expressive power of programming languages
- LCF considered as a programming language
- A theory of type polymorphism in programming
- A syntactic theory of dynamic binding
- Typability and type checking in System F are equivalent and undecidable
- Unchecked exceptions can be strictly more powerful than call/cc
- A type-theoretical alternative to ISWIM, CUCH, OWHY
- Modelling environments in call-by-value programming languages.
- Edinburgh LCF. A mechanized logic of computation
- Algebraic operations and generic effects
- Relating computational effects by \(\top \top \)-lifting
- A static simulation of dynamic delimited control
- Combining effects: sum and tensor
- A Classical Realizability Model for a Semantical Value Restriction
- Two Cotensors in One: Presentations of Algebraic Theories for Local State and Fresh Names
- Dependent Types and Fibred Computational Effects
- Algebraic Effects, Linearity, and Quantum Programming Languages
- Handling Algebraic Effects
- Inferring Algebraic Effects
- Implementing first-class polymorphic delimited continuations by a type-directed selective CPS-transform
- Fusion for Free
- Algebraic foundations for effect-dependent optimisations
- Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages
- Operations on records
- Polymorphic Delimited Continuations
- Data types à la carte
- Completeness for Algebraic Theories of Local State
- A Substructural Type System for Delimited Continuations
- Focalisation and Classical Realisability
- Efficient algebraic effect handlers for Prolog
- Trace semantics for polymorphic references
- An Algebraic Presentation of Predicate Logic
- Local States in String Diagrams
- Compiling standard ML to Java bytecodes
- Programming and reasoning with algebraic effects and dependent types
- Handlers in action
- The marriage of effects and monads
- Instances of Computational Effects: An Algebraic Perspective
- Functional and Logic Programming
- Type directed compilation of row-typed algebraic effects
- Do be do be do
- Parametric effect monads and semantics of effect systems
- Typed Dynamic Control Operators for Delimited Continuations
- Delimited dynamic binding
- The Mechanical Evaluation of Expressions
- A certified implementation of ML with structural polymorphism and recursive types
- An Effect System for Algebraic Effects and Handlers
- An introduction to algebraic effects and handlers (invited tutorial paper)
This page was built for publication: No value restriction is needed for algebraic effects and handlers
