Edit Profile (opens in new tab) Uustalu, Tarmo Compute Distance To: Compute Author ID: uustalu.tarmo Published as: Uustalu, Tarmo; Uustalu, T. Homepage: http://cs.ioc.ee/~tarmo/ External Links: MGP · ORCID · dblp · GND Documents Indexed: 72 Publications since 1990 9 Contributions as Editor Co-Authors: 36 Co-Authors with 70 Joint Publications 572 Co-Co-Authors all top 5 Co-Authors 10 single-authored 16 Vene, Varmo 10 Veltri, Niccolò 8 Chapman, James T. E. 5 Ahman, Danel 5 Altenkirch, Thorsten 5 Nakata, Keiko 4 Capretta, Venanzio 4 Ghani, Neil 4 Matthes, Ralph 4 Saabas, Ando 4 Zeilberger, Noam 3 Firsov, Denis 3 Katsumata, Shin-ya 3 Pinto, Luís F. 3 Vain, Jüri 2 Abel, Andreas M. 2 Tyugu, Ènn Kharal’dovich 1 Barthe, Gilles 1 Bezem, Marc 1 Breuvart, Flavien 1 Frade, Maria João 1 Gaboardi, Marco 1 Hamana, Makoto 1 Hasuo, Ichiro 1 Jacobs, Bart 1 Johann, Patricia 1 Laud, Peeter 1 Lorents, Peeter 1 Maarand, Hendrik 1 Mayoh, Brian H. 1 Orchard, Dominic A. 1 Pardo, Alberto 1 Pinto, Linu 1 Rivas, Exequiel 1 Sato, Tetsuya 1 Voorneveld, Niels F. W. all top 5 Serials 5 Theoretical Computer Science 5 Logical Methods in Computer Science 4 Journal of Logical and Algebraic Methods in Programming 3 The Journal of Logic and Algebraic Programming 3 Lecture Notes in Computer Science 2 MSCS. Mathematical Structures in Computer Science 2 Nordic Journal of Computing 2 Proceedings of the Estonian Academy of Sciences. Physics, Mathematics 2 RAIRO. Theoretical Informatics and Applications 2 Journal of Formalized Reasoning 1 Science of Computer Programming 1 Information and Computation 1 Journal of Logic and Computation 1 Izvestiya Akademii Nauk Èstonskoĭ SSR. Fizika. Matematika 1 Journal of Functional Programming 1 Informatica (Vilnius) 1 Higher-Order and Symbolic Computation 1 Fundamenta Informaticae 1 LIPIcs – Leibniz International Proceedings in Informatics all top 5 Fields 70 Computer science (68-XX) 26 Category theory; homological algebra (18-XX) 25 Mathematical logic and foundations (03-XX) 9 General and overarching topics; collections (00-XX) 1 General algebraic systems (08-XX) 1 Group theory and generalizations (20-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 54 Publications have been cited 269 times in 183 Documents Cited by ▼ Year ▼ Type-based termination of recursive definitions. Zbl 1054.68027Barthe, G.; Frade, M. J.; Giménez, E.; Pinto, L.; Uustalu, T. 18 2004 Primitive (co)recursion and course-of-value (co) iteration, categorically. Zbl 0935.68011Uustalu, Tarmo; Vene, Varmo 16 1999 Iteration and coiteration schemes for higher-order and nested datatypes. Zbl 1070.68093Abel, Andreas; Matthes, Ralph; Uustalu, Tarmo 16 2005 Generalizing substitution. Zbl 1042.18003Uustalu, Tarmo 15 2003 Monads need not be endofunctors. Zbl 1284.18010Altenkirch, Thorsten; Chapman, James; Uustalu, Tarmo 14 2010 Monads need not be endofunctors. Zbl 1448.18007Altenkirch, Thorsten; Chapman, James; Uustalu, Tarmo 12 2015 Comonadic notions of computation. Zbl 1279.68088Uustalu, Tarmo; Vene, Varmo 12 2008 Proof search and counter-model construction for bi-intuitionistic propositional logic with labelled sequents. Zbl 1260.03105Pinto, Luís; Uustalu, Tarmo 10 2009 Substitution in non-wellfounded syntax with variable binding. Zbl 1071.68063Matthes, Ralph; Uustalu, Tarmo 10 2004 Coproducts of ideal monads. Zbl 1072.18006Ghani, Neil; Uustalu, Tarmo 9 2004 Mendler-style inductive types, categorically. Zbl 0937.68029Uustalu, Tarmo; Vene, Varmo 8 1999 Recursion schemes from comonads. Zbl 0994.68018Uustalu, Tarmo; Vene, Varmo; Pardo, Alberto 8 2001 Corecursive algebras: a study of general structured corecursion. Zbl 1266.68083Capretta, Venanzio; Uustalu, Tarmo; Vene, Varmo 7 2009 Recursive coalgebras from comonads. Zbl 1110.68068Capretta, Venanzio; Uustalu, Tarmo; Vene, Varmo 6 2006 Combining effects and coeffects via grading. Zbl 1361.68037Gaboardi, Marco; Katsumata, Shin-ya; Orchard, Dominic; Breuvart, Flavien; Uustalu, Tarmo 6 2016 Explicit substitutions and higher-order syntax. Zbl 1105.68021Ghani, Neil; Uustalu, Tarmo; Hamana, Makoto 6 2006 A Hoare logic for the coinductive trace-based big-step semantics of While. Zbl 1260.68111Nakata, Keiko; Uustalu, Tarmo 5 2010 A compositional natural semantics and Hoare logic for low-level languages. Zbl 1111.68071Saabas, Ando; Uustalu, Tarmo 5 2007 Program and proof optimizations with type systems. Zbl 1151.68008Saabas, Ando; Uustalu, Tarmo 5 2008 When is a container a comonad? Zbl 1338.68172Ahman, Danel; Chapman, James; Uustalu, Tarmo 5 2014 Functional programming with apomorphisms (corecursion). Zbl 0963.68028Vene, Varmo; Uustalu, Tarmo 4 1998 A compositional natural semantics and Hoare logic for low-level languages. Zbl 1273.68215Saabas, Ando; Uustalu, Tarmo 4 2006 Type systems equivalent to data-flow analyses for imperative languages. Zbl 1153.68351Laud, Peeter; Uustalu, Tarmo; Vene, Varmo 4 2006 On streams that are finitely red. Zbl 1267.03058Bezem, Marc; Nakata, Keiko; Uustalu, Tarmo 4 2012 Trace-based coinductive operational semantics for While. Big-step and small-step, relational and functional styles. Zbl 1252.68056Nakata, Keiko; Uustalu, Tarmo 4 2009 A divertimento on MonadPlus and nondeterminism. Zbl 1355.68041Uustalu, Tarmo 3 2016 Update monads: cointerpreting directed containers. Zbl 1359.68049Ahman, Danel; Uustalu, Tarmo 3 2014 Substitution in non-wellfounded syntax with variable binding. Zbl 1270.68089Matthes, Ralph; Uustalu, Tarmo 3 2003 Generalized iteration and coiteration for higher-order nested datatypes. Zbl 1029.68097Abel, Andreas; Matthes, Ralph; Uustalu, Tarmo 3 2003 Monadic augment and generalised short cut fusion. Zbl 1302.68079Ghani, Neil; Johann, Patricia; Uustalu, Tarmo; Vene, Varmo 3 2005 A Hoare logic for the coinductive trace-based big-step semantics of While. Zbl 1448.68281Nakata, Keiko; Uustalu, Tarmo 3 2015 Quotienting the delay monad by weak bisimilarity. Zbl 1407.68305Chapman, James; Uustalu, Tarmo; Veltri, Niccolò 3 2015 Build, augment and destroy, universally. Zbl 1116.68490Ghani, Neil; Uustalu, Tarmo; Vene, Varmo 3 2004 Normalization by evaluation for \(\lambda ^{\rightarrow 2}\). Zbl 1122.68393Altenkirch, Thorsten; Uustalu, Tarmo 3 2004 Coherence for skew-monoidal categories. Zbl 1464.18018Uustalu, Tarmo 3 2014 Least and greatest fixed points in intuitionistic natural deduction. Zbl 0984.68136Uustalu, Tarmo; Vene, Varmo 3 2002 Codensity lifting of monads and its dual. Zbl 1398.18005Katsumata, Shin-Ya; Sato, Tetsuya; Uustalu, Tarmo 2 2018 Quotienting the delay monad by weak bisimilarity. Zbl 1407.68306Chapman, James; Uustalu, Tarmo; Veltri, Niccolò 2 2019 Container combinatorics: monads and Lax monoidal functors. Zbl 06839854Uustalu, Tarmo 2 2017 The recursion scheme from the cofree recursive comonad. Zbl 1291.68149Uustalu, Tarmo; Vene, Varmo 2 2011 Relative monads formalised. Zbl 1451.68330Altenkirch, Thorsten; Chapman, James; Uustalu, Tarmo 2 2014 Recursive coalgebras from comonads. Zbl 1271.18005Capretta, Venanzio; Uustalu, Tarmo; Vene, Varmo 1 2004 The essence of dataflow programming. Zbl 1156.68378Uustalu, Tarmo; Vene, Varmo 1 2006 Coalgebraic update lenses. Zbl 1337.68084Ahman, Danel; Uustalu, Tarmo 1 2014 A coalgebraic view of bar recursion and bar induction. Zbl 1474.03105Capretta, Venanzio; Uustalu, Tarmo 1 2016 Certified CYK parsing of context-free languages. Zbl 1371.68137Firsov, Denis; Uustalu, Tarmo 1 2014 Certified parsing of regular languages. Zbl 1303.68077Firsov, Denis; Uustalu, Tarmo 1 2013 When is a container a comonad? Zbl 1338.68171Ahman, Danel; Chapman, James; Uustalu, Tarmo 1 2012 Resumptions, weak bisimilarity and big-step semantics for While with interactive I/O: an exercise in mixed induction-coinduction. Zbl 1455.68100Nakata, Keiko; Uustalu, Tarmo 1 2010 Proof optimization for partial redundancy elimination. Zbl 1187.68167Saabas, Ando; Uustalu, Tarmo 1 2009 Finiteness and rational sequences, constructively. Zbl 1418.68069Uustalu, Tarmo; Veltri, Niccolò 1 2017 The delay monad and restriction categories. Zbl 1444.18010Uustalu, Tarmo; Veltri, Niccolò 1 2017 Formalizing restriction categories. Zbl 1451.68338Chapman, James; Uustalu, Tarmo; Veltri, Niccolò 1 2017 Proof theory of partially normal skew monoidal categories. Zbl 1477.18041Uustalu, Tarmo; Veltri, Niccolò; Zeilberger, Noam 1 2021 Proof theory of partially normal skew monoidal categories. Zbl 1477.18041Uustalu, Tarmo; Veltri, Niccolò; Zeilberger, Noam 1 2021 Quotienting the delay monad by weak bisimilarity. Zbl 1407.68306Chapman, James; Uustalu, Tarmo; Veltri, Niccolò 2 2019 Codensity lifting of monads and its dual. Zbl 1398.18005Katsumata, Shin-Ya; Sato, Tetsuya; Uustalu, Tarmo 2 2018 Container combinatorics: monads and Lax monoidal functors. Zbl 06839854Uustalu, Tarmo 2 2017 Finiteness and rational sequences, constructively. Zbl 1418.68069Uustalu, Tarmo; Veltri, Niccolò 1 2017 The delay monad and restriction categories. Zbl 1444.18010Uustalu, Tarmo; Veltri, Niccolò 1 2017 Formalizing restriction categories. Zbl 1451.68338Chapman, James; Uustalu, Tarmo; Veltri, Niccolò 1 2017 Combining effects and coeffects via grading. Zbl 1361.68037Gaboardi, Marco; Katsumata, Shin-ya; Orchard, Dominic; Breuvart, Flavien; Uustalu, Tarmo 6 2016 A divertimento on MonadPlus and nondeterminism. Zbl 1355.68041Uustalu, Tarmo 3 2016 A coalgebraic view of bar recursion and bar induction. Zbl 1474.03105Capretta, Venanzio; Uustalu, Tarmo 1 2016 Monads need not be endofunctors. Zbl 1448.18007Altenkirch, Thorsten; Chapman, James; Uustalu, Tarmo 12 2015 A Hoare logic for the coinductive trace-based big-step semantics of While. Zbl 1448.68281Nakata, Keiko; Uustalu, Tarmo 3 2015 Quotienting the delay monad by weak bisimilarity. Zbl 1407.68305Chapman, James; Uustalu, Tarmo; Veltri, Niccolò 3 2015 When is a container a comonad? Zbl 1338.68172Ahman, Danel; Chapman, James; Uustalu, Tarmo 5 2014 Update monads: cointerpreting directed containers. Zbl 1359.68049Ahman, Danel; Uustalu, Tarmo 3 2014 Coherence for skew-monoidal categories. Zbl 1464.18018Uustalu, Tarmo 3 2014 Relative monads formalised. Zbl 1451.68330Altenkirch, Thorsten; Chapman, James; Uustalu, Tarmo 2 2014 Coalgebraic update lenses. Zbl 1337.68084Ahman, Danel; Uustalu, Tarmo 1 2014 Certified CYK parsing of context-free languages. Zbl 1371.68137Firsov, Denis; Uustalu, Tarmo 1 2014 Certified parsing of regular languages. Zbl 1303.68077Firsov, Denis; Uustalu, Tarmo 1 2013 On streams that are finitely red. Zbl 1267.03058Bezem, Marc; Nakata, Keiko; Uustalu, Tarmo 4 2012 When is a container a comonad? Zbl 1338.68171Ahman, Danel; Chapman, James; Uustalu, Tarmo 1 2012 The recursion scheme from the cofree recursive comonad. Zbl 1291.68149Uustalu, Tarmo; Vene, Varmo 2 2011 Monads need not be endofunctors. Zbl 1284.18010Altenkirch, Thorsten; Chapman, James; Uustalu, Tarmo 14 2010 A Hoare logic for the coinductive trace-based big-step semantics of While. Zbl 1260.68111Nakata, Keiko; Uustalu, Tarmo 5 2010 Resumptions, weak bisimilarity and big-step semantics for While with interactive I/O: an exercise in mixed induction-coinduction. Zbl 1455.68100Nakata, Keiko; Uustalu, Tarmo 1 2010 Proof search and counter-model construction for bi-intuitionistic propositional logic with labelled sequents. Zbl 1260.03105Pinto, Luís; Uustalu, Tarmo 10 2009 Corecursive algebras: a study of general structured corecursion. Zbl 1266.68083Capretta, Venanzio; Uustalu, Tarmo; Vene, Varmo 7 2009 Trace-based coinductive operational semantics for While. Big-step and small-step, relational and functional styles. Zbl 1252.68056Nakata, Keiko; Uustalu, Tarmo 4 2009 Proof optimization for partial redundancy elimination. Zbl 1187.68167Saabas, Ando; Uustalu, Tarmo 1 2009 Comonadic notions of computation. Zbl 1279.68088Uustalu, Tarmo; Vene, Varmo 12 2008 Program and proof optimizations with type systems. Zbl 1151.68008Saabas, Ando; Uustalu, Tarmo 5 2008 A compositional natural semantics and Hoare logic for low-level languages. Zbl 1111.68071Saabas, Ando; Uustalu, Tarmo 5 2007 Recursive coalgebras from comonads. Zbl 1110.68068Capretta, Venanzio; Uustalu, Tarmo; Vene, Varmo 6 2006 Explicit substitutions and higher-order syntax. Zbl 1105.68021Ghani, Neil; Uustalu, Tarmo; Hamana, Makoto 6 2006 A compositional natural semantics and Hoare logic for low-level languages. Zbl 1273.68215Saabas, Ando; Uustalu, Tarmo 4 2006 Type systems equivalent to data-flow analyses for imperative languages. Zbl 1153.68351Laud, Peeter; Uustalu, Tarmo; Vene, Varmo 4 2006 The essence of dataflow programming. Zbl 1156.68378Uustalu, Tarmo; Vene, Varmo 1 2006 Iteration and coiteration schemes for higher-order and nested datatypes. Zbl 1070.68093Abel, Andreas; Matthes, Ralph; Uustalu, Tarmo 16 2005 Monadic augment and generalised short cut fusion. Zbl 1302.68079Ghani, Neil; Johann, Patricia; Uustalu, Tarmo; Vene, Varmo 3 2005 Type-based termination of recursive definitions. Zbl 1054.68027Barthe, G.; Frade, M. J.; Giménez, E.; Pinto, L.; Uustalu, T. 18 2004 Substitution in non-wellfounded syntax with variable binding. Zbl 1071.68063Matthes, Ralph; Uustalu, Tarmo 10 2004 Coproducts of ideal monads. Zbl 1072.18006Ghani, Neil; Uustalu, Tarmo 9 2004 Build, augment and destroy, universally. Zbl 1116.68490Ghani, Neil; Uustalu, Tarmo; Vene, Varmo 3 2004 Normalization by evaluation for \(\lambda ^{\rightarrow 2}\). Zbl 1122.68393Altenkirch, Thorsten; Uustalu, Tarmo 3 2004 Recursive coalgebras from comonads. Zbl 1271.18005Capretta, Venanzio; Uustalu, Tarmo; Vene, Varmo 1 2004 Generalizing substitution. Zbl 1042.18003Uustalu, Tarmo 15 2003 Substitution in non-wellfounded syntax with variable binding. Zbl 1270.68089Matthes, Ralph; Uustalu, Tarmo 3 2003 Generalized iteration and coiteration for higher-order nested datatypes. Zbl 1029.68097Abel, Andreas; Matthes, Ralph; Uustalu, Tarmo 3 2003 Least and greatest fixed points in intuitionistic natural deduction. Zbl 0984.68136Uustalu, Tarmo; Vene, Varmo 3 2002 Recursion schemes from comonads. Zbl 0994.68018Uustalu, Tarmo; Vene, Varmo; Pardo, Alberto 8 2001 Primitive (co)recursion and course-of-value (co) iteration, categorically. Zbl 0935.68011Uustalu, Tarmo; Vene, Varmo 16 1999 Mendler-style inductive types, categorically. Zbl 0937.68029Uustalu, Tarmo; Vene, Varmo 8 1999 Functional programming with apomorphisms (corecursion). Zbl 0963.68028Vene, Varmo; Uustalu, Tarmo 4 1998 all cited Publications top 5 cited Publications all top 5 Cited by 217 Authors 25 Uustalu, Tarmo 12 Milius, Stefan 9 Abel, Andreas M. 9 Adámek, Jiří 8 Goncharov, Sergeĭ Savost’yanovich 8 Veltri, Niccolò 7 Schröder, Lutz 7 Velebil, Jiří 6 Ahrens, Benedikt 6 Ghani, Neil 6 Matthes, Ralph 6 Orchard, Dominic A. 6 Rauch, Christoph 5 Johann, Patricia 4 Altenkirch, Thorsten 4 Capretta, Venanzio 4 Fiore, Marcelo P. 4 Jacobs, Bart 4 Katsumata, Shin-ya 4 Piróg, Maciej 4 Staton, Sam 4 Vene, Varmo 4 Zeilberger, Noam 3 Ahman, Danel 3 Blanqui, Frédéric 3 Dagnino, Francesco 3 Gibbons, Jeremy 3 Hasuo, Ichiro 3 Saabas, Ando 3 Stump, Aaron 2 Allais, Guillaume 2 Atkey, Robert 2 Berger, Ulrich 2 Beringer, Lennart 2 Bove, Ana 2 Chapman, James T. E. 2 Chaudhuri, Kaustuv 2 Czajka, Łukasz 2 Dal Lago, Ugo 2 Eades, Harley III 2 El-Zawawy, Mohamed A. 2 Firsov, Denis 2 Galmiche, Didier 2 Hamana, Makoto 2 Hinze, Ralf 2 Hirschowitz, André 2 Hutton, Graham 2 Hyland, J. Martin E. 2 Jaskelioff, Mauro 2 Jenkins, Christopher 2 Kozen, Dexter C. 2 Lima, Leonardo B. 2 Maggesi, Marco 2 McBride, Conor Thomas 2 Méry, Daniel 2 Miranda Perea, Favio Ezequiel 2 Mörtberg, Anders 2 Pientka, Brigitte 2 Reis, Giselle 2 Rennela, Mathys 2 Rivas, Exequiel 2 Sato, Tetsuya 2 Schäfer, Steven 2 Silva, Alexandra 2 Torrini, Paolo 2 van der Weide, Niels 2 Wu, Nicolas 1 Abou-Saleh, Faris 1 Abramsky, Samson 1 Adelsberger, Stephan 1 Affeldt, Reynald 1 Ahn, Ki Yung 1 Ancona, Davide 1 Andrianopoulos, Jim 1 Asada, Kazuyuki 1 Avron, Arnon 1 Bacci, Giorgio 1 Bacelar Almeida, José 1 Bach Poulsen, Casper 1 Backes, Julian 1 Barthe, Gilles 1 Benton, Nick 1 Bertot, Yves 1 Brown, Chad Edward 1 Bubel, Richard 1 Chifflier, Pierre 1 Clarke, Bryce 1 Clarke, Dave 1 Coquand, Thierry 1 Cruttwell, Geoffrey 1 Danielsson, Nils Anders 1 de Boer, Frank S. 1 De Nicola, Rocco 1 De Queiroz, Ruy José Guerra Barretto 1 Devesas Campos, Marco 1 Diehl, Larry 1 Din, Crystal Chang 1 Dyckhoff, Roy 1 Eades III, Harley 1 Feltey, Daniel ...and 117 more Authors all top 5 Cited in 23 Serials 17 Theoretical Computer Science 17 Journal of Functional Programming 16 Logical Methods in Computer Science 10 MSCS. Mathematical Structures in Computer Science 7 Information and Computation 5 RAIRO. Theoretical Informatics and Applications 4 Science of Computer Programming 3 Journal of Automated Reasoning 3 The Journal of Logic and Algebraic Programming 3 Journal of Logical and Algebraic Methods in Programming 2 Journal of Pure and Applied Algebra 2 Formal Aspects of Computing 2 Applied Categorical Structures 2 Journal of the Egyptian Mathematical Society 2 Theory and Applications of Categories 2 Higher-Order and Symbolic Computation 1 Journal of Computer and System Sciences 1 Archive for Mathematical Logic 1 Selecta Mathematica. New Series 1 Computer Languages, Systems & Structures 1 Journal of Applied Logic 1 Tbilisi Mathematical Journal 1 The Review of Symbolic Logic all top 5 Cited in 14 Fields 156 Computer science (68-XX) 63 Mathematical logic and foundations (03-XX) 58 Category theory; homological algebra (18-XX) 5 General algebraic systems (08-XX) 2 Measure and integration (28-XX) 2 Algebraic topology (55-XX) 1 General and overarching topics; collections (00-XX) 1 Order, lattices, ordered algebraic structures (06-XX) 1 Dynamical systems and ergodic theory (37-XX) 1 Probability theory and stochastic processes (60-XX) 1 Quantum theory (81-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 1 Systems theory; control (93-XX) 1 Information and communication theory, circuits (94-XX) Citations by Year