Zobrazeno 1 - 10
of 72
pro vyhledávání: '"Lhotak, Ondrej"'
Autor:
Lee, Edward, Zhao, Yaoyu, You, James, Satheeskumar, Kavin, Lhoták, Ondřej, Brachthäuser, Jonathan
Publikováno v:
Proc. ACM Program. Lang. 8, OOPSLA1, Article 115 (April 2024), 30 pages
Type qualifiers offer a lightweight mechanism for enriching existing type systems to enforce additional, desirable, program invariants. They do so by offering a restricted but effective form of subtyping. While the theory of type qualifiers is well u
Externí odkaz:
http://arxiv.org/abs/2311.07480
Autor:
Lee, Edward, Lhoták, Ondřej
Reference immutability is a type based technique for taming mutation that has long been studied in the context of object-oriented languages, like Java. Recently, though, languages like Scala have blurred the lines between functional programming langu
Externí odkaz:
http://arxiv.org/abs/2307.04960
Autor:
Odersky, Martin, Boruch-Gruszecki, Aleksander, Lee, Edward, Brachthäuser, Jonathan, Lhoták, Ondřej
Type systems usually characterize the shape of values but not their free variables. However, many desirable safety properties could be guaranteed if one knew the free variables captured by values. We describe CCsubBox, a calculus where such captured
Externí odkaz:
http://arxiv.org/abs/2207.03402
Autor:
Boruch-Gruszecki, Aleksander, Brachthäuser, Jonathan Immanuel, Lee, Edward, Lhoták, Ondřej, Odersky, Martin
Type systems usually characterize the shape of values but not their free variables. However, there are many desirable safety properties one could guarantee if one could track how references can escape. For example, one may implement algebraic effect
Externí odkaz:
http://arxiv.org/abs/2105.11896
Event-driven programming is widely used for implementing user interfaces, web applications, and non-blocking I/O. An event-driven program is organized as a collection of event handlers whose execution is triggered by events. Traditional static analys
Externí odkaz:
http://arxiv.org/abs/1910.12935
Autor:
Hu, Jason, Lhoták, Ondřej
Dependent Object Types (DOT) is a calculus with path dependent types, intersection types, and object self-references, which serves as the core calculus of Scala 3. Although the calculus has been proven sound, it remains open whether type checking in
Externí odkaz:
http://arxiv.org/abs/1908.05294
Autor:
Rapoport, Marianna, Lhoták, Ondřej
The Dependent Object Types (DOT) calculus aims to formalize the Scala programming language with a focus on path-dependent types $-$ types such as $x.a_1\dots a_n.T$ that depend on the runtime value of a path $x.a_1\dots a_n$ to an object. Unfortunate
Externí odkaz:
http://arxiv.org/abs/1904.07298
Dependent Object Types (DOT) is intended to be a core calculus for modelling Scala. Its distinguishing feature is abstract type members, fields in objects that hold types rather than values. Proving soundness of DOT has been surprisingly challenging,
Externí odkaz:
http://arxiv.org/abs/1706.03814
Relying on ubiquitous Internet connectivity, applications on mobile devices frequently perform web requests during their execution. They fetch data for users to interact with, invoke remote functionalities, or send user-generated content or meta-data
Externí odkaz:
http://arxiv.org/abs/1705.06629
Autor:
Rapoport, Marianna, Lhoták, Ondřej
The Dependent Object Types (DOT) calculus aims to model the essence of Scala, with a focus on abstract type members, path-dependent types, and subtyping. Other Scala features could be defined by translation to DOT. Mutation is a fundamental feature o
Externí odkaz:
http://arxiv.org/abs/1611.07610