scholarly journals Handling delimited continuations with dependent types

2018 ◽  
Vol 2 (ICFP) ◽  
pp. 1-31 ◽  
Author(s):  
Youyou Cong ◽  
Kenichi Asai
Keyword(s):  
Dependent Types ◽  
Delimited Continuations

scholarly journals Effekt: Capability-passing style for type- and effect-safe, extensible effect handlers in Scala

2020 ◽  
Vol 30 ◽  
Author(s):  
JONATHAN IMMANUEL BRACHTHÄUSER ◽  
PHILIPP SCHUSTER ◽  
KLAUS OSTERMANN
Keyword(s):  
Type System ◽  
Dependent Types ◽  
Individual Effect ◽  
Library Design ◽  
Programming Paradigm ◽  
Intersection Types ◽  
Delimited Continuations ◽  
Path Dependent

Abstract Effect handlers are a promising way to structure effectful programs in a modular way. We present the Scala library Effekt, which is centered around capability passing and implemented in terms of a monad for multi-prompt delimited continuations. Effekt is the first library implementation of effect handlers that supports effect safety and effect polymorphism without resorting to type-level programming. We describe a novel way of achieving effect safety using intersection types and path-dependent types. The effect system of our library design fits well into the programming paradigm of capability passing and is inspired by the effect system of Zhang & Myers (2019, Proc. ACM Program. Lang.3(POPL), 5:1-5:29). Capabilities carry an abstract type member, which represents an individual effect type and reflects the use of the capability on the type level. We represent effect rows as the contravariant intersection of effect types. Handlers introduce capabilities and remove components of the intersection type. Reusing the existing type system of Scala, we get effect subtyping and effect polymorphism for free.

scholarly journals Secure distributed programming with value-dependent types

2011 ◽  
Author(s):  
Nikhil Swamy ◽  
Juan Chen ◽  
Cédric Fournet ◽  
Pierre-Yves Strub ◽  
Karthikeyan Bhargavan ◽  
...  
Keyword(s):  
Distributed Programming ◽  
Dependent Types

Foundations of path-dependent types

2014 ◽  
Vol 49 (10) ◽  
pp. 233-249 ◽  
Author(s):  
Nada Amin ◽  
Tiark Rompf ◽  
Martin Odersky
Keyword(s):  
Dependent Types ◽  
Path Dependent

scholarly journals A Type System for Dynamic Delimited Continuations

2008 ◽  
Vol 4 ◽  
pp. 182-192 ◽  
Author(s):  
Takuo Yonezawa ◽  
Yukiyoshi Kameyama
Keyword(s):  
Type System ◽  
Delimited Continuations

scholarly journals Semantics with Dependent Types for Indefinites

2016 ◽  
Vol 46 (1) ◽  
pp. 173-192
Author(s):  
Justyna Grudzińska
Keyword(s):  
Dynamic Properties ◽  
Formal System ◽  
Dependent Types ◽  
Generalized Quantifiers

Abstract The paper proposes a new semantics with dependent types for indefinites, encompassing both the data related to their exceptional scopal behavior and the data related to their anaphoric (dynamic) properties. The proposal builds on the formal system combining generalized quantifiers ([Mostowski 1957], [Lindström 1966]) with dependent types ([Martin-Löf 1972], [Makkai 1995]) in [Grudzińska & Zawadowski 2014] and [Grudzińska & Zawadowski 2016].

Sign in / Sign up

Export Citation Format

Share Document