default search action
Tarmo Uustalu
Person information
- affiliation: Reykjavik University, Iceland
- affiliation (former): Tallinn University of Technology, Dept. of Software Science, Estonia
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
- [c83]Sergey Goncharov, Tarmo Uustalu:
A Unifying Categorical View of Nondeterministic Iteration and Tests. CONCUR 2024: 25:1-25:22 - [c82]Exequiel Rivas
, Tarmo Uustalu
Concurrent monads for shared state. PPDP 2024: 19:1-19:13 - [i7]Sergey Goncharov, Tarmo Uustalu:
A Unifying Categorical View of Nondeterministic Iteration and Tests. CoRR abs/2407.08688 (2024) - 2023
- [c81]Silvio Capobianco
Additive Cellular Automata Graded-Monadically. PPDP 2023: 13:1-13:9 - 2022
- [j38]José Espírito Santo
Plotkin's call-by-value λ-calculus as a modal calculus. J. Log. Algebraic Methods Program. 127: 100775 (2022) - [j37]Shin-ya Katsumata
Flexible presentations of graded monads. Proc. ACM Program. Lang. 6(ICFP): 902-930 (2022) - [c80]Dylan McDermott
Sweedler Theory of Monads. FoSSaCS 2022: 428-448 - [c79]Dylan McDermott
A Type System with Subtyping for WebAssembly's Stack Polymorphism. ICTAC 2022: 305-323 - [c78]Dylan McDermott
Flexibly Graded Monads and Graded Algebras. MPC 2022: 102-128 - [c77]Flavien Breuvart, Dylan McDermott
Canonical Gradings of Monads. ACT 2022: 1-21 - [c76]Dylan McDermott
What Makes a Strong Monad? MSFP@ETAPS 2022: 113-133 - [c75]Tarmo Uustalu
Proof Theory of Skew Non-Commutative MILL. NCL 2022: 118-135 - 2021
- [j36]Hendrik Maarand
Operational semantics with semicommutations. J. Log. Algebraic Methods Program. 121: 100677 (2021) - 2020
- [c74]Tarmo Uustalu
Algebraic and Coalgebraic Perspectives on Interaction Laws. APLAS 2020: 186-205 - [c73]Shin-ya Katsumata
Interaction Laws of Monads and Comonads. LICS 2020: 604-618 - [c72]Tarmo Uustalu
Eilenberg-Kelly Reloaded. MFPS 2020: 233-256 - [c71]Dylan McDermott
Degrading Lists. PPDP 2020: 6:1-6:14 - [c70]Tarmo Uustalu
Deductive Systems and Coherence for Skew Prounital Closed Categories. LFMTP 2020: 35-53 - [c69]Tarmo Uustalu
Proof Theory of Partially Normal Skew Monoidal Categories. ACT 2020: 230-246 - [i6]Tarmo Uustalu, Niccolò Veltri, Noam Zeilberger
The Sequent Calculus of Skew Monoidal Categories. CoRR abs/2003.05213 (2020)
2010 – 2019
- 2019
- [j35]Hendrik Maarand
Certified normalization of generalized traces. Innov. Syst. Softw. Eng. 15(3-4): 253-265 (2019) - [j34]James Chapman
Quotienting the delay monad by weak bisimilarity. Math. Struct. Comput. Sci. 29(1): 67-92 (2019) - [c68]Danel Ahman
Decomposing Comonad Morphisms. CALCO 2019: 14:1-14:19 - [c67]Hendrik Maarand
Reordering Derivatives of Trace Closures of Regular Languages. CONCUR 2019: 40:1-40:16 - [c66]José Espírito Santo
Modal Embeddings and Calling Paradigms. FSCD 2019: 18:1-18:20 - [i5]Hendrik Maarand
Reordering Derivatives of Trace Closures of Regular Languages (Full Version). CoRR abs/1908.03551 (2019) - [i4]Shin-ya Katsumata, Exequiel Rivas, Tarmo Uustalu
Interaction laws of monads and comonads. CoRR abs/1912.13477 (2019) - 2018
- [j33]Shin-ya Katsumata
Codensity Lifting of Monads and its Dual. Log. Methods Comput. Sci. 14(4) (2018) - [j32]Luís Pinto
A proof-theoretic study of bi-intuitionistic propositional sequent calculus. J. Log. Comput. 28(1): 165-202 (2018) - [c65]Hendrik Maarand
Certified Foata Normalization for Generalized Traces. NFM 2018: 299-314 - [c64]Tarmo Uustalu
The Sequent Calculus of Skew Monoidal Categories. MFPS 2018: 345-370 - [e7]Bernd Fischer, Tarmo Uustalu
Theoretical Aspects of Computing - ICTAC 2018 - 15th International Colloquium, Stellenbosch, South Africa, October 16-19, 2018, Proceedings. Lecture Notes in Computer Science 11187, Springer 2018, ISBN 978-3-030-02507-6 [contents] - [e6]Tarmo Uustalu:
21st International Conference on Types for Proofs and Programs, TYPES 2015, May 18-21, 2015, Tallinn, Estonia. LIPIcs 69, Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2018, ISBN 978-3-95977-030-9 [contents] - [i3]Shin-ya Katsumata, Tetsuya Sato, Tarmo Uustalu:
Codensity Lifting of Monads and its Dual. CoRR abs/1810.07972 (2018) - 2017
- [j31]Tarmo Uustalu
Finiteness and rational sequences, constructively. J. Funct. Program. 27: e13 (2017) - [j30]James Chapman
Formalizing Restriction Categories. J. Formaliz. Reason. 10(1): 1-36 (2017) - [c63]Tarmo Uustalu
Partiality and Container Monads. APLAS 2017: 406-425 - [c62]Danel Ahman, Tarmo Uustalu:
Taking Updates Seriously. BX@ETAPS 2017: 59-73 - [c61]Tarmo Uustalu
The Delay Monad and Restriction Categories. ICTAC 2017: 32-50 - [c60]Tarmo Uustalu
Container Combinatorics: Monads and Lax Monoidal Functors. TTCS 2017: 91-105 - [c59]Hendrik Maarand
Generating Representative Executions [Extended Abstract]. PLACES@ETAPS 2017: 39-48 - 2016
- [j29]Tarmo Uustalu
A divertimento on MonadPlus and nondeterminism. J. Log. Algebraic Methods Program. 85(5): 1086-1094 (2016) - [j28]Tarmo Uustalu
Guest editors' foreword. J. Log. Algebraic Methods Program. 85(6): 1109 (2016) - [c58]Venanzio Capretta
A Coalgebraic View of Bar Recursion and Bar Induction. FoSSaCS 2016: 91-106 - [c57]Marco Gaboardi
Combining effects and coeffects via grading. ICFP 2016: 476-489 - [c56]Denis Firsov
Variations on Noetherianness. MSFP 2016: 76-88 - [c55]Danel Ahman
Directed Containers as Categories. MSFP 2016: 89-98 - 2015
- [j27]Thorsten Altenkirch
Monads need not be endofunctors. Log. Methods Comput. Sci. 11(1) (2015) - [j26]Keiko Nakata, Tarmo Uustalu
A Hoare logic for the coinductive trace-based big-step semantics of While. Log. Methods Comput. Sci. 11(1) (2015) - [c54]Denis Firsov
Certified Normalization of Context-Free Grammars. CPP 2015: 167-174 - [c53]Denis Firsov
Dependently typed programming with finite sets. WGP@ICFP 2015: 33-44 - [c52]James Chapman
Quotienting the Delay Monad by Weak Bisimilarity. ICTAC 2015: 110-125 - [c51]Tarmo Uustalu
Stateful Runners of Effectful Computations. MFPS 2015: 403-421 - 2014
- [j25]Danel Ahman
When is a container a comonad? Log. Methods Comput. Sci. 10(3) (2014) - [j24]Thorsten Altenkirch, James Chapman, Tarmo Uustalu:
Relative Monads Formalised. J. Formaliz. Reason. 7(1): 1-43 (2014) - [j23]Denis Firsov
Certified CYK parsing of context-free languages. J. Log. Algebraic Methods Program. 83(5-6): 459-468 (2014) - [c50]Tarmo Uustalu
Coherence for Skew-Monoidal Categories. MSFP 2014: 68-77 - [c49]Danel Ahman
Coalgebraic Update Lenses. MFPS 2014: 25-48 - 2013
- [j22]Ralph Matthes
Preface. RAIRO Theor. Informatics Appl. 47(1): 1-2 (2013) - [c48]Denis Firsov
Certified Parsing of Regular Languages. CPP 2013: 98-113 - [c47]Danel Ahman
Update Monads: Cointerpreting Directed Containers. TYPES 2013: 1-23 - [c46]Tarmo Uustalu
Coinductive Big-Step Semantics for Concurrency. PLACES 2013: 63-78 - [e5]Greg Morrisett, Tarmo Uustalu:
ACM SIGPLAN International Conference on Functional Programming, ICFP'13, Boston, MA, USA - September 25 - 27, 2013. ACM 2013, ISBN 978-1-4503-2326-0 [contents] - [i2]Ichiro Hasuo
Coinduction for Computation Structures and Programming Languages (NII Shonan Meeting 2013-11). NII Shonan Meet. Rep. 2013 (2013) - 2012
- [j21]Marc Bezem, Keiko Nakata, Tarmo Uustalu
On streams that are finitely red. Log. Methods Comput. Sci. 8(4) (2012) - [c45]Tarmo Uustalu
Explicit Binds: Effortless Efficiency with and without Trees. FLOPS 2012: 317-331 - [c44]Danel Ahman
When Is a Container a Comonad? FoSSaCS 2012: 74-88 - [c43]Tarmo Uustalu
Structured general corecursion and coinductive graphs [extended abstract]. FICS 2012: 55-61 - 2011
- [c42]Keiko Nakata, Tarmo Uustalu
A Proof Pearl with the Fan Theorem and Bar Induction - Walking through Infinite Trees with Mixed Induction and Coinduction. APLAS 2011: 353-368 - 2010
- [j20]Thorsten Altenkirch
Preface. Fundam. Informaticae 102(2) (2010) - [j19]Tarmo Uustalu
Guest Editors' Foreword. J. Log. Algebraic Methods Program. 79(7): 435 (2010) - [c41]Keiko Nakata, Tarmo Uustalu
A Hoare Logic for the Coinductive Trace-Based Big-Step Semantics of While. ESOP 2010: 488-506 - [c40]Tarmo Uustalu:
A Note on Strong Dinaturality, Initial Algebras and Uniform Parameterized Fixpoint Operators. FICS 2010: 77-82 - [c39]Thorsten Altenkirch
Monads Need Not Be Endofunctors. FoSSaCS 2010: 297-311 - [c38]Tarmo Uustalu
Antifounded Coinduction in Type Theory. PAR@ITP 2010: 114 - [c37]Silvio Capobianco, Tarmo Uustalu:
A Categorical Outlook on Cellular Automata. JAC 2010: 88-99 - [c36]Keiko Nakata, Tarmo Uustalu
Resumptions, Weak Bisimilarity and Big-Step Semantics for While with Interactive I/O: An Exercise in Mixed Induction-Coinduction. SOS 2010: 57-75 - [c35]Luís Pinto
Relating Sequent Calculi for Bi-intuitionistic Propositional Logic. CL&C 2010: 57-72 - [i1]Silvio Capobianco, Tarmo Uustalu:
A Categorical Outlook on Cellular Automata. CoRR abs/1012.1220 (2010)
2000 – 2009
- 2009
- [j18]Conor McBride
Preface. J. Funct. Program. 19(3-4): 263-264 (2009) - [j17]Ando Saabas, Tarmo Uustalu
Proof optimization for partial redundancy elimination. J. Log. Algebraic Methods Program. 78(7): 619-642 (2009) - [j16]Tarmo Uustalu
Preface. Sci. Comput. Program. 74(8): 497 (2009) - [c34]Maria João Frade
Bidirectional data-flow analyses, type-systematically. PEPM 2009: 141-150 - [c33]Venanzio Capretta
Corecursive Algebras: A Study of General Structured Corecursion. SBMF 2009: 84-100 - [c32]Luís Pinto
Proof Search and Counter-Model Construction for Bi-intuitionistic Propositional Logic with Labelled Sequents. TABLEAUX 2009: 295-309 - [c31]Bernd Fischer
Program Repair as Sound Optimization of Broken Programs. TASE 2009: 165-173 - [c30]Keiko Nakata, Tarmo Uustalu
Trace-Based Coinductive Operational Semantics for While. TPHOLs 2009: 375-390 - [e4]Ralph Matthes, Tarmo Uustalu:
6th Workshop on Fixed Points in Computer Science, FICS 2009, Coimbra, Portugal, September 12-13, 2009. Institute of Cybernetics 2009, ISBN 978-9949-430-29-1 [contents] - 2008
- [j15]Ando Saabas, Tarmo Uustalu
Program and proof optimizations with type systems. J. Log. Algebraic Methods Program. 77(1-2): 131-154 (2008) - [c29]Ando Saabas, Tarmo Uustalu
Proof optimization for partial redundancy elimination. PEPM 2008: 91-101 - [c28]Tarmo Uustalu
The Recursion Scheme from the Cofree Recursive Comonad. MSFP@ICALP 2008: 135-157 - [c27]Tarmo Uustalu
Comonadic Notions of Computation. CMCS 2008: 263-284 - 2007
- [j14]Ando Saabas, Tarmo Uustalu
A compositional natural semantics and Hoare logic for low-level languages. Theor. Comput. Sci. 373(3): 273-302 (2007) - [c26]Ichiro Hasuo, Bart Jacobs, Tarmo Uustalu
Categorical Views on Computations on Trees (Extended Abstract). ICALP 2007: 619-630 - [c25]Maria João Frade
Foundational certification of data-flow analyses. TASE 2007: 107-116 - [c24]Ando Saabas, Tarmo Uustalu
Type Systems for Optimizing Stack-based Code. Bytecode@ETAPS 2007: 103-119 - 2006
- [j13]Venanzio Capretta
Recursive coalgebras from comonads. Inf. Comput. 204(4): 437-468 (2006) - [j12]Neil Ghani, Tarmo Uustalu
Explicit substitutions and higher-order syntax. High. Order Symb. Comput. 19(2-3): 263-282 (2006) - [j11]Peeter Laud
Type systems equivalent to data-flow analyses for imperative languages. Theor. Comput. Sci. 364(3): 292-310 (2006) - [c23]Ando Saabas, Tarmo Uustalu:
Compositional Type Systems for Stack-Based Low-Level Languages. CATS 2006: 27-39 - [e3]Tarmo Uustalu
Mathematics of Program Construction, 8th International Conference, MPC 2006, Kuressaare, Estonia, July 3-5, 2006, Proceedings. Lecture Notes in Computer Science 4014, Springer 2006, ISBN 3-540-35631-2 [contents] - [e2]Conor McBride, Tarmo Uustalu:
Workshop on Mathematically Structured Functional Programming, MSFP@MPC 2006, Kuressaare, Estonia, July 2, 2006. Workshops in Computing, BCS 2006 [contents] - 2005
- [j10]Tarmo Uustalu, Varmo Vene:
Signals and Comonads. J. Univers. Comput. Sci. 11(7): 1310-1326 (2005) - [j9]Andreas Abel, Ralph Matthes
Iteration and coiteration schemes for higher-order and nested datatypes. Theor. Comput. Sci. 333(1-2): 3-66 (2005) - [c22]Tarmo Uustalu
The Essence of Dataflow Programming. APLAS 2005: 2-18 - [c21]Tarmo Uustalu, Varmo Vene:
The Essence of Dataflow Programming. CEFP 2005: 135-167 - [c20]Neil Ghani, Patricia Johann, Tarmo Uustalu
Monadic augment and generalised short cut fusion. ICFP 2005: 294-305 - [c19]Tarmo Uustalu, Varmo Vene:
Comonadic functional attribute evaluation. Trends in Functional Programming 2005: 145-162 - [c18]Ando Saabas, Tarmo Uustalu
A Compositional Natural Semantics and Hoare Logic for Low-Level Languages. SOS@ICALP 2005: 151-168 - [e1]Varmo Vene, Tarmo Uustalu
Advanced Functional Programming, 5th International School, AFP 2004, Tartu, Estonia, August 14-21, 2004, Revised Lectures. Lecture Notes in Computer Science 3622, Springer 2005, ISBN 3-540-28540-7 [contents] - 2004
- [j8]Neil Ghani, Tarmo Uustalu
Coproducts of Ideal Monads. RAIRO Theor. Informatics Appl. 38(4): 321-342 (2004) - [j7]Gilles Barthe
Type-based termination of recursive definitions. Math. Struct. Comput. Sci. 14(1): 97-141 (2004) - [j6]Ralph Matthes
Substitution in non-wellfounded syntax with variable binding. Theor. Comput. Sci. 327(1-2): 155-174 (2004) - [c17]Neil Ghani, Tarmo Uustalu
Build, Augment and Destroy, Universally. APLAS 2004: 327-347 - [c16]Thorsten Altenkirch, Tarmo Uustalu
Normalization by Evaluation for lambda-2. FLOPS 2004: 260-275 - [c15]Neil Ghani, Tarmo Uustalu, Varmo Vene:
Generalizing the AUGMENT combinator. Trends in Functional Programming 2004: 65-78 - [c14]Venanzio Capretta
Recursive Coalgebras from Comonads. CMCS 2004: 43-61 - 2003
- [j5]Tarmo Uustalu
Generalizing Substitution. RAIRO Theor. Informatics Appl. 37(4): 315-336 (2003) - [c13]Neil Ghani, Tarmo Uustalu:
Coproducts of Ideal Monads (Extended Abstract). FICS 2003: 32-36 - [c12]Tarmo Uustalu, Varmo Vene:
An Alternative Characterization of Complete Iterativeness (Extended Abstract). FICS 2003: 81-83 - [c11]Andreas Abel, Ralph Matthes, Tarmo Uustalu
Generalized Iteration and Coiteration for Higher-Order Nested Datatypes. FoSSaCS 2003: 54-69 - [c10]Neil Ghani, Tarmo Uustalu
Explicit substitutions and higher-order syntax. MERLIN 2003 - [c9]Ralph Matthes, Tarmo Uustalu
Substitution in Non-wellfounded Syntax with Variable Binding. CMCS 2003: 191-205 - 2002
- [j4]Tarmo Uustalu
Least and greatest fixed points in intuitionistic natural deduction. Theor. Comput. Sci. 272(1-2): 315-339 (2002) - [c8]Tarmo Uustalu:
Generalizing substitution. FICS 2002: 9-11 - [c7]Gilles Barthe
CPS translating inductive and coinductive types. PEPM 2002: 131-142 - [c6]Tarmo Uustalu
Monad Translating Inductive and Coinductive Types. TYPES 2002: 299-315 - 2001
- [j3]Tarmo Uustalu, Varmo Vene, Alberto Pardo:
Recursion Schemes from Comonads. Nord. J. Comput. 8(3): 366-390 (2001) - [c5]Tarmo Uustalu:
(Co)monads from inductive and coinductive types (Extended Abstract). APPIA-GULP-PRODE 2001: 47-61 - [c4]Tarmo Uustalu, Varmo Vene:
The Dual of Substitution is Redecoration. Scottish Functional Programming Workshop 2001: 99-110
1990 – 1999
- 1999
- [j2]Tarmo Uustalu, Varmo Vene:
Primitive (Co)Recursion and Course-of-Value (Co)Iteration, Categorically. Informatica 10(1): 5-26 (1999) - [j1]Tarmo Uustalu, Varmo Vene:
Mendler-Style Inductive Types, Categorically. Nord. J. Comput. 6(3): 343- (1999) - 1993
- [c3]Brian H. Mayoh, Enn Tyugu, Tarmo Uustalu
Constraint Satisfaction and Constraint Programming: A Brief Lead-In. NATO ASI CP 1993: 1-16 - [c2]Enn Tyugu, Tarmo Uustalu
Higher-Order Functional Constraint Networks. NATO ASI CP 1993: 116-139 - 1992
- [c1]Tarmo Uustalu:
Combining Object-Oriented and Logic Paradigms: A Modal Logic Programming Approach. ECOOP 1992: 98-113
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-10-09 20:32 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: