Tarmo Uustalu
Current Organizations / Institutes
The organizations/institutes from the scholar's latest article
Previous Organizations / Institutes
The organizations / institutes from the scholar's other articles in the past ten years
Research Subjects
Tarmo Uustalu has a total of 60 co-authors. Here are the top co-authors by number of shared publications:
- Varmo Vene
University of Tartu
13 shared publications - Niccolò Veltri
Tallinn University of Technology
8 shared publications Ando Saabas
6 shared publications- Danel Ahman
University of Tartu, Tartu, Estonia
6 shared publications - James Chapman
IOHK
6 shared publications Keiko Nakata
Institute of Cybernetics Tallinn University of Technology Akadeemia tee 21 12618 Tallinn Estonia
6 shared publications
Latest Publications
- 20 July 2026
- Published by Springer Nature
- p. 162-177
Glivenko’s Theorem Underneath Structure
- Open Access
- 9 September 2024
- Published by Association for Computing Machinery (ACM)
- p. 1-13
Concurrent monads for shared state
In the monad-based approach to functional programming with effects, sequential composition, the primary high-level control structure for combining effectful functions, takes a special role. In this article, we advocate the idea that parallel composition should be recognized as a high-level control structure on an equal footing with sequential composition. We promote the concept of concurrent monad, which axiomatizes both sequential and parallel composition, and illustrate the approach by describing two concurrent monads for interleaving shared state concurrency: one of resumptions, the other of collections of traces.
- 9 September 2024
- Published by Association for Computing Machinery (ACM)
- p. 1-13
Open AccessConcurrent monads for shared state
In the monad-based approach to functional programming with effects, sequential composition, the primary high-level control structure for combining effectful functions, takes a special role. In this article, we advocate the idea that parallel composition should be recognized as a high-level control structure on an equal footing with sequential composition. We promote the concept of concurrent monad, which axiomatizes both sequential and parallel composition, and illustrate the approach by describing two concurrent monads for interleaving shared state concurrency: one of resumptions, the other of collections of traces.
- Open Access
- 22 October 2023
- Published by Association for Computing Machinery (ACM)
- p. 1-9
Additive Cellular Automata Graded-Monadically
Cellular automata are an archetypical comonadic notion of computation in that computation happens in the coKleisli category of a comonad. In this paper, we show that they can also be viewed as graded comonadic—a perspective that turns out to be both more informative and also more basic. We also discuss additive cellular automata to show that they admit both a graded comonadic and a graded monadic view. That these two perspectives are simultaneously available in this special case arises from a graded version of an observation by Kleiner about adjoint comonad-monad pairs.
- 22 October 2023
- Published by Association for Computing Machinery (ACM)
- p. 1-9
Open AccessAdditive Cellular Automata Graded-Monadically
Cellular automata are an archetypical comonadic notion of computation in that computation happens in the coKleisli category of a comonad. In this paper, we show that they can also be viewed as graded comonadic—a perspective that turns out to be both more informative and also more basic. We also discuss additive cellular automata to show that they admit both a graded comonadic and a graded monadic view. That these two perspectives are simultaneously available in this special case arises from a graded version of an observation by Kleiner about adjoint comonad-monad pairs.
- 3 October 2022
- Published by Springer Nature
- p. 305-323
A Type System with Subtyping for WebAssembly’s Stack Polymorphism
- 3 October 2022
- Published by Springer Nature
- p. 305-323
A Type System with Subtyping for WebAssembly’s Stack Polymorphism
- Open Access
- 29 August 2022
- Published by Association for Computing Machinery (ACM) in Proceedings of the ACM on Programming Languages
- Vol. 6 (ICFP) , 902-930
Flexible presentations of graded monads
A large class of monads used to model computational effects have natural presentations by operations and equations, for example, the list monad can be presented by a constant and a binary operation subject to unitality and associativity. Graded monads are a generalization of monads that enable us to track quantitative information about the effects being modelled. Correspondingly, a large class of graded monads can be presented using an existing notion of graded presentation. However, the existing notion has some deficiencies, in particular many effects do not have natural graded presentations. We introduce a notion of flexibly graded presentation that does not suffer from these issues, and develop the associated theory. We show that every flexibly graded presentation induces a graded monad equipped with interpretations of the operations of the presentation, and that all graded monads satisfying a particular condition on colimits have a flexibly graded presentation. As part of this, we show that the usual algebra-preserving correspondence between presentations and a class of monads transfers to an algebra-preserving correspondence between flexibly graded presentations and a class of flexibly graded monads.
- 29 August 2022
- Published by Association for Computing Machinery (ACM) in Proceedings of the ACM on Programming Languages
- Vol. 6 (ICFP) , 902-930
Open AccessFlexible presentations of graded monads
A large class of monads used to model computational effects have natural presentations by operations and equations, for example, the list monad can be presented by a constant and a binary operation subject to unitality and associativity. Graded monads are a generalization of monads that enable us to track quantitative information about the effects being modelled. Correspondingly, a large class of graded monads can be presented using an existing notion of graded presentation. However, the existing notion has some deficiencies, in particular many effects do not have natural graded presentations. We introduce a notion of flexibly graded presentation that does not suffer from these issues, and develop the associated theory. We show that every flexibly graded presentation induces a graded monad equipped with interpretations of the operations of the presentation, and that all graded monads satisfying a particular condition on colimits have a flexibly graded presentation. As part of this, we show that the usual algebra-preserving correspondence between presentations and a class of monads transfers to an algebra-preserving correspondence between flexibly graded presentations and a class of flexibly graded monads.
- 4 April 2022
- Published by Elsevier in Journal of Logical and Algebraic Methods in Programming
- Vol. 127
Plotkin's call-by-value λ-calculus as a modal calculus
- 4 April 2022
- Published by Elsevier in Journal of Logical and Algebraic Methods in Programming
- Vol. 127
Plotkin's call-by-value λ-calculus as a modal calculus
- Open Access
- 29 March 2022
- Published by Springer Nature
- p. 428-448
Sweedler Theory of Monads
Monad-comonad interaction laws are a mathematical concept for describing communication protocols between effectful computations and coeffectful environments in the paradigm where notions of effectful computation are modelled by monads and notions of coeffectful environment by comonads. We show that monad-comonad interaction laws are an instance of measuring maps from Sweedler theory for duoidal categories whereby the final interacting comonad for a monad and a residual monad arises as the Sweedler hom and the initial residual monad for a monad and an interacting comonad as the Sweedler copower. We then combine this with a (co)algebraic characterization of monad-comonad interaction laws to derive descriptions of the Sweedler hom and the Sweedler copower in terms of their coalgebras resp. algebras.
- 29 March 2022
- Published by Springer Nature
- p. 428-448
Open AccessSweedler Theory of Monads
Monad-comonad interaction laws are a mathematical concept for describing communication protocols between effectful computations and coeffectful environments in the paradigm where notions of effectful computation are modelled by monads and notions of coeffectful environment by comonads. We show that monad-comonad interaction laws are an instance of measuring maps from Sweedler theory for duoidal categories whereby the final interacting comonad for a monad and a residual monad arises as the Sweedler hom and the initial residual monad for a monad and an interacting comonad as the Sweedler copower. We then combine this with a (co)algebraic characterization of monad-comonad interaction laws to derive descriptions of the Sweedler hom and the Sweedler copower in terms of their coalgebras resp. algebras.
- 1 June 2021
- Published by Elsevier in Journal of Logical and Algebraic Methods in Programming
- Vol. 121
Operational semantics with semicommutations
- 1 June 2021
- Published by Elsevier in Journal of Logical and Algebraic Methods in Programming
- Vol. 121
Operational semantics with semicommutations