Tarmo Uustalu's research papers

• T. Uustalu, N. Voorneveld. Algebraic and coalgebraic perspectives on interaction laws.
  In B. C. d. S. Oliveira, ed., Proc. of 18th Asian Symp. on Programming Languages and Systems, APLAS 2020 (Fukuoka, Nov./Dec. 2020), Lect. Notes in Comput. Sci., Springer, to appear.
• D. McDermott, M. Piróg, T. Uustalu. Degrading lists.
  In Proc. of 22nd Int. Symp. on Principles and Practice of Programming Languages, PPDP 2020 (Bologna, Sept. 2020), Int. Conf. Proc. Series, article 6, 14 pp. ACM Press, 2020. doi:10.1145/3414080.3414084 (© the authors) - pdf, Haskell code (exotic list monads)
• T. Uustalu, N. Veltri, N. Zeilberger. Proof theory of partially normal skew monoidal categories.
  In D. Spivak, J. Vicary, eds., Proc. of 3rd Applied Category Theory Conf. (Cambridge, MA, July 2020), Electron. Proc. in Theor. Comput. Sci., Open Publishing Assoc., to appear. article at publisher (open access) (© the authors) - video
• T. Uustalu, N. Veltri, N. Zeilberger. Eilenberg-Kelly reloaded.
  Electron. Notes in Theor. Comput. Sci. (P. Johann, ed., Proc. of 36th Conf. on Mathematical Foundations of Programming Semantics, MFPS XXXVI (Paris, June 2020), to appear. - pdf, slides, video
• H. Maarand, T. Uustalu. Operational semantics with semicommutations.
  Manuscript, submitted.
• S. Katsumata, E. Rivas, T. Uustalu. Interaction laws of monads and comonads.
  Full version as arXiv eprint 1912.13477, 2019. arXiv:1912.13477 //
  Conf. version in Proc. of 35th Ann. ACM/IEEE Symp. on Logic in Computer Science, LICS 2020 (Saarbrücken, July 2020), pp. 604-618. ACM Press, 2020. doi:10.1145/3373718.3394808 (© the authors) - pdf, slides, video
• H. Maarand, T. Uustalu. Reordering derivatives of trace closures of regular languages.
  Full version as arXiv eprint 1908.03551, 2019. arXiv:1908.03551 //
  Conf. version in W. Fokkink, R. van Glabbeek, eds., Proc. of 30th Int. Conf. on Concurrency Theory, CONCUR 2019 (Amsterdam, Aug. 2019), v. 140 of Leibniz. Int. Proc. in Inf., article 40. Dagstuhl Publishing, 2019. doi:10.4230/lipics.concur.2019.40 (open access) (© the authors) - errata, video from Estonian-Latvian CS Theory Days in Pärnu
• D. Ahman, T. Uustalu. Decomposing comonad morphisms.
  In M. Roggenbach, A. Sokolova, eds., Proc. of 8th Conf. on Algebra and Coalgebra in Computer Science, CALCO 2019 (London, June 2019), v. 139 of Leibniz Int. Proc. in Inf., article 14. Dagstuhl Publishing, 2019. doi:10.4230/lipics.calco.2019.14 (open access) (© the authors)
• J. Espírito Santo, L. Pinto, T. Uustalu. Modal embeddings and calling paradigms.
  In H. Geuvers, ed., Proc. of 4th Int. Conf. on Formal Structures for Computation and Deduction, FSCD 2019 (Dortmund, June 2019), v. 131 of Leibniz Int. Proc. in Inf., article 18. Dagstuhl Publishing, 2019. doi:10.4230/lipics.fscd.2019.18 (open access) (© the authors)
• T. Uustalu, N. Veltri, N. Zeilberger. The sequent calculus of skew monoidal categories.
  In C. Casadio, P. J. Scott, eds., Joachim Lambek: The Interplay of Mathematics, Logic, and Linguistics, Outstanding Contributions to Logic, Springer, to appear. (© the authors) //
  Conf. version in Electron. Notes in Theor. Comput. Sci., v. 341 (S. Staton, ed., Proc. of 34th Conf. on Mathematical Foundations of Programming Semantics, MFPS XXXIV, Halifax, NS, June 2018), pp. 345-370, 2018. doi:10.1016/j.entcs.2018.11.017 (open access) (© the authors)
• H. Maarand, T. Uustalu. Certified normalization of generalized traces.
  Innov. in Softw. and Syst. Engin., v. 15, n. 3-4, pp. 253-265, 2019. doi:10.1007/s11334-019-00347-1 (© Springer) //
  Conf. version titled Certified Foata normalization for generalized traces in A. Dutle, C. Muñoz, A. Narkawicz, eds., Proc. of 10th NASA Formal Methods Symp., NFM 2018 (Newport News, VA, Apr. 2018), v. 10811 of Lect. Notes in Comput. Sci., pp. 299-314. Springer, 2018. doi:10.1007/978-3-319-77935-5_21 (© Springer) - pdf
• T. Uustalu, N. Veltri. Partiality and container monads.
  In B.-Y. E. Chang, ed., Proc. of 15th Asian Symp. on Programming Languages and Systems, APLAS 2017 (Suzhou, Nov. 2017), v. 10695 of Lect. Notes in Comput. Sci., pp. 406-425. Springer, 2017. doi:10.1007/978-3-319-71237-6_20 (© Springer) - pdf
• T. Uustalu. Container combinatorics: monads and lax monoidal functors.
  In M. R. Mousavi, J. Sgall, eds., Proc. of 2nd IFIP WG 1.8 Int. Conf. on Topics in Theoretical Computer Science, TTCS 2017 (Tehran, Sept. 2017), v. 10608 of Lect. Notes in Comput. Sci., pp. 91-105. Springer, 2017. doi:10.1007/978-3-319-68953-1_8 (© IFIP) - pdf
• H. Maarand, T. Uustalu. Generating representative executions (extended abstract).
  In V. T. Vasconcelos, P. Haller, eds., Proc. of 10th Wksh. on Programming Language Approaches to Concurrency and Communication-Centric Software, PLACES 2017 (Uppsala, Apr. 2017), v. 246 of Electron. Proc. in Theor. Comput. Sci., pp. 39-48. Open Publishing Assoc., 2017. doi:10.4204/eptcs.246.8 (open access)
• D. Ahman, T. Uustalu. Taking updates seriously.
  In R. Eramo, M. Johnson, eds., Proc. of 6th Int. Wksh. on Bidirectional Transformations, BX 2017 (Uppsala, Apr. 2017), v. 1827 of CEUR Wksh. Proc., pp. 59-73. RWTH Aachen, 2017. article at publisher (open access)
• T. Uustalu, N. Veltri. The delay monad and restriction categories.
  In D. V. Hung, D. Kapur, eds., Proc. of 14th Int. Coll. on Theoretical Aspects of Computing, ICTAC 2017 (Hanoi, Oct. 2017), v. 10580 of Lect. Notes in Comput. Sci., pp. 32-50. Springer, 2017. doi:10.1007/978-3-319-67729-3_3 (© Springer) - pdf
• M. Gaboardi, S. Katsumata, D. Orchard, F. Breuvart, T. Uustalu. Combining effects and coeffects via grading.
  Reprinted in ACM SIGPLAN Notices, v. 51, n. 9, pp. 476-489, 2016. doi:10.1145/3022670.2951939 //
  In Proc. of 21st ACM SIGPLAN Int. Conf. on Functional Programming, ICFP '16 (Nara, Sept. 2016), pp. 476-489. ACM Press, 2016. doi:10.1145/2951913.2951939 (© the authors) - free pdf via ACM Author-Izer, video
• T. Uustalu, N. Veltri. Finiteness and rational sequences, constructively.
  J. of Funct. Program., v. 27, article e13, 2017. doi:10.1017/s0956796817000041 (© Cambridge University Press)
• D. Ahman, T. Uustalu. Directed containers as categories.
  In R. Atkey, N. Krishnaswami, eds., Proc. of 6th Wksh. on Mathematically Structured Functional Programming, MSFP 2016 (Eindhoven, April 2016), v. 207 of Electron. Proc. in Theor. Comput. Sci., pp. 89-98. Open Publishing Assoc., 2016. doi:10.4204/eptcs.207.5 (open access) - errata
• D. Firsov, T. Uustalu, N. Veltri. Variations on Noetherianness.
  In R. Atkey, N. Krishnaswami, eds., Proc. of 6th Wksh. on Mathematically Structured Functional Programming, MSFP 2016 (Eindhoven, April 2016), v. 207 of Electron. Proc. in Theor. Comput. Sci., pp. 76-88. Open Publishing Assoc., 2016. doi:10.4204/eptcs.207.4 (open access)
• S. Katsumata, T. Sato, T. Uustalu. Codensity lifting of monads and its dual.
  Log. Methods in Comput. Sci., v. 14, n. 4, article 6, 2018. doi:10.23638/lmcs-14(4:6)2018 (open access) (© the authors)
• L. Pinto, T. Uustalu. A proof theoretic-study of bi-intuitionistic propositional sequent calculus.
  J. of Log. and Comput., v. 28, n. 1, pp. 165-202, 2018. doi:10.1093/logcom/exx044 (© the authors) - pdf
• V. Capretta, T. Uustalu. A coalgebraic view of bar recursion and bar induction.
  In B. Jacobs, C. Löding, eds., Proc. of 19th Int. Conf. on Foundations of Software Science and Computation Structures, FoSSaCS 2016 (Eindhoven, April 2016), v. 9634 of Lect. Notes in Comput. Sci., pp. 91-106. Springer, 2016. doi:10.1007/978-3-662-49630-5_6 (© Springer) - pdf
• T. Uustalu. A divertimento on MonadPlus and nondeterminism.
  J. of Log. and Algebraic Methods in Program., v. 85, n. 5, part 2, pp. 1086-1094, 2016. doi:10.1016/j.jlamp.2016.06.004 (open access) (© Elsevier Science)
  Extended abstract distributed at 4th ACM SIGPLAN Wksh. on Higher-Order Programming with Effects, HOPE 2015, Vancouver, BC, Aug. 2015. - video
• J. Chapman, T. Uustalu, N. Veltri. Quotienting the delay monad by weak bisimilarity.
  Math. Struct. in Comput. Sci., v. 29, n. 1, pp. 67-92, 2019. doi:10.1017/s0960129517000184 (© Cambridge University Press) //
  Conf. version in M. Leucker, C. Rueda, F. D. Valencia, eds., Proc. of 12th Int. Coll. on Theoretical Aspects of Computing, ICTAC 2015 (Cali, Oct. 2015), v. 9399 of Lect. Notes in Comput. Sci., pp. 110-125. Springer, 2015. doi:10.1007/978-3-319-25150-9_8 (© Springer) - pdf
• D. Firsov, T. Uustalu. Dependently typed programming with finite sets.
  In Proc. of 11th ACM SIGPLAN Wksh. on Generic Programming, WGP '15 (Vancouver, BC, Aug. 2015), pp. 33-44. ACM Press, 2015. doi:10.1145/2808098.2808102 (© the authors) - free pdf via ACM Author-Izer
• T. Uustalu. Stateful runners for effectful computations.
  Electron. Notes in Theor. Comput. Sci., v. 319 (D. Ghica, ed., Proc. of 31st Conf. on Mathematical Foundations of Programming Semantics, MFPS XXXI, Nijmegen, June 2015), pp. 403-421, 2015. doi:10.1016/j.entcs.2015.12.024 (open access) (© Elsevier Science)
• D. Firsov, T. Uustalu. Certified normalization of context-free grammars.
  In Proc. of 2015 ACM Conf. on Certified Programs and Proofs, CPP '15 (Mumbai, Jan. 2015), pp. 167-174. ACM Press, 2015. doi:10.1145/2676724.2693177 (© the authors) - free pdf via ACM Author-Izer
• D. Ahman, T. Uustalu. Coalgebraic update lenses.
  Electron. Notes in Theor. Comput. Sci., v. 308 (B. Jacobs, A. Silva, S. Staton, eds., Proc. of 30th Conf. on Mathematical Foundations of Programming Semantics, MFPS XXX, Ithaca, NY, June 2014), pp. 25-48, 2014. doi:10.1016/j.entcs.2014.10.003 (open access) (© Elsevier Science)
• T. Uustalu. Coherence for skew-monoidal categories.
  In N. Krishnaswami, P. Levy, eds., Proc. of 5th Wksh. on Mathematically Structured Functional Programming, MSFP 2014 (Grenoble, Apr. 2014), v. 153 of Electron. Proc. in Theor. Comput. Sci., pp. 68-77. Open Publishing Assoc., 2014. doi:10.4204/eptcs.153.5 (open access) - Agda code
• D. Ahman, T. Uustalu. Update monads: cointerpreting directed containers.
  In R. Matthes, A. Schubert, eds., Proc. of 19th Conf. on Types for Proofs and Programs, TYPES 2013 (Toulouse, Apr. 2013), v. 26 of Leibniz Int. Proc. in Inform, pp. 1-23. Dagstuhl Publishing, 2014. doi:10.4230/lipics.types.2013.1 (open access) (© the authors)
• J. Chapman, T. Uustalu, N. Veltri. Formalizing restriction categories.
  J. of Formaliz. Reason., v. 10, n. 1, pp. 1-36, 2017. doi:10.6092/issn.1972-5787/6237 (open access) (© the authors)
• D. Firsov, T. Uustalu. Certified CYK parsing of context-free languages.
  J. of Log. and Algebraic Meth. in Program., v. 83, n. 5-6, pp. 459-468, 2014. doi:10.1016/j.jlamp.2014.09.002 (open access) (© Elsevier Science)
• D. Firsov, T. Uustalu. Certified parsing of regular languages.
  In G. Gonthier, M. Norrish, eds., Proc. of 3rd Int. Conf. on Certified Programs and Proofs, CPP 2013 (Melbourne, Dec. 2013), v. 8307 of Lect. Notes in Comput. Sci., pp. 98-113. Springer, 2013. doi:10.1007/978-3-319-03545-1_7 (© Springer) - pdf
• T. Uustalu. Coinductive big-step semantics for concurrency.
  In W. Vanderbauwhede, N. Yoshida, eds., Proc. of 6th Wksh. on Programming Language Approaches to Concurrency and Communication-Centric Software, PLACES 2013 (Rome, March 2013), v. 137 of Electron. Proc. in Theor. Comput. Sci., pp. 63-78. Open Publishing Assoc., 2013. doi:10.4204/eptcs.137.6 (open access) - Haskell code
• D. Ahman, T. Uustalu. Distributive laws of directed containers.
  Progress in Informatics, v. 10, pp. 3-18, 2013. doi:10.2201/niipi.2013.10.2 (open access) - Haskell code //
  Extended abstract in L. Schröder, D. Pattinson, eds., Short Contributions of 11th Int. Wksh. on Coalgebraic Methods in Comput. Sci., CMCS '12 (Tallinn, March/April 2012), pp. 1-3. Inst. of Cybernetics, 2012. - pdf
• T. Uustalu. Structured general corecursion and coinductive graphs (extended abstract).
  In Z. Ésik, D. Miller, eds., Proc. of 8th Wksh. on Fixed Points in Computer Science, FICS 2012 (Tallinn, March 2012), v. 77 of Electron. Proc. in Theor. Comput. Sci., pp. 55-61. Open Publishing Assoc., 2012. doi:10.4204/eptcs.77.8 (open access)
• T. Uustalu. Explicit binds: effortless efficiency with and without trees.
  In T. Schrijvers, P. Thiemann, eds., Proc. of 11th Int. Symp. on Functional and Logic Programming, FLOPS 2012 (Kobe, May 2012), v. 7294 of Lect. Notes in Comput. Sci., pp. 317-331. Springer, 2012. doi:10.1007/978-3-642-29822-6_25 (© Springer) - pdf, Haskell code
• D. Ahman, J. Chapman, T. Uustalu. When is a container a comonad?
  Log. Methods in Comput. Sci., v. 10, n. 3, article 14, 2014. doi:10.2168/lmcs-10(3:14)2014 (open access) (© the authors) //
  Conf. version in L. Birkedal, ed., Proc. of 15th Int. Conf. on Foundations of Software Science and Computation Structures, FoSSaCS 2012 (Tallinn, March 2012), v. 7213 of Lect. Notes in Comput. Sci., pp. 74-88. Springer, 2012. doi:10.1007/978-3-642-28729-9_5 (© Springer) - pdf, project page, incl. Agda code
• K. Nakata, T. Uustalu, M. Bezem. A proof pearl with the fan theorem and bar induction: walking through infinite trees with mixed induction and coinduction.
  In H. Yang, ed., Proc. of 9th Asian Symp. on Programming Languages and Systems, APLAS 2011 (Kenting, Dec. 2011), v. 7078 of Lect. Notes in Comput. Sci., pp. 353-368. Springer, 2011. doi:10.1007/978-3-642-25318-8_26 (© Springer) - pdf
• M. Bezem, K. Nakata, T. Uustalu. On streams that are finitely red.
  Log. Methods in Comput. Sci., v. 8, n. 4, article 4, 2012. doi:10.2168/lmcs-8(4:4)2012 (open access) (© the authors)
• S. Capobianco, T. Uustalu. A categorical outlook on cellular automata.
  In J. Kari, ed., Proc. of 2nd Symp. on Cellular Automata, JAC 2010 (Turku, Dec. 2010), v. 13 of TUCS Lecture Notes, pp. 88-99. Turku Centre for Computer Science, 2010. - pdf
• L. Pinto, T. Uustalu. Relating sequent calculi for bi-intuitionistic propositional logic.
  In S. van Bakel, S. Berardi, U. Berger, eds., Proc. of 3rd Wksh. on Classical Logic and Computation CL&C 2010 (Brno, Aug. 2010), v. 47 of Electron. Proc. in Theor. Comput. Sci., pp. 57-72. Open Publishing Assoc., 2011. doi:10.4204/eptcs.47.7 (open access)
• T. Uustalu. A note on strong dinaturality, initial algebras and uniform parameterized fixpoint operators (extended abstract).
  In L. Santocanale, ed., Proc. of 7th Wksh. on Fixed Points in Computer Science, FICS 2010 (Brno, Aug. 2010), pp. 77-82. Masarykova Univ., 2010. - pdf
• K. Nakata, T. Uustalu. Resumptions, weak bisimilarity and big-step semantics for While with interactive I/O: an exercise in mixed induction-coinduction.
  In L. Aceto, P. Sobocinski, eds., Proc. of 7th Wksh. on Structural Operational Semantics, SOS 2010 (Paris, Aug. 2010), v. 32 of Electron. Proc. in Theor. Comput. Sci., pp. 57-75. Open Publishing Assoc., 2010. doi:10.4204/eptcs.32.5 (open access)
• T. Uustalu. Strong relative monads (extended abstract).
  In B. Jacobs, M. Niqui, J. Rutten, A. Silva, eds., Short Contributions of 10th Int. Wksh. on Coalgebraic Methods in Comput. Sci., CMCS '10 (Paphos, March 2010), pp. 23-24. CWI, 2010. - pdf
• T. Altenkirch, J. Chapman, T. Uustalu. Relative monads formalised.
  J. of Formaliz. Reason., v. 7, n. 1, pp. 1-43, 2014. doi:10.6092/issn.1972-5787/4389 (open access) (© the authors)
• T. Altenkirch, J. Chapman, T. Uustalu. Monads need not be endofunctors.
  Log. Methods in Comput. Sci., v. 11, n. 1, article 3, 2015. doi:10.2168/lmcs-11(1:3)2015 (open access) (© the authors) //
  Conf. version in L. Ong, ed., Proc. of 13th Int. Conf. on Foundations of Software Science and Computation Structures, FoSSaCS 2010 (Paphos, March 2010), v. 6014 of Lect. Notes in Comput. Sci., pp. 297-311. Springer, 2010. doi:10.1007/978-3-642-12032-9_21 (© Springer) - pdf
• K. Nakata, T. Uustalu. A Hoare logic for the coinductive trace-based big-step semantics of While.
  Log. Methods in Comput. Sci., v. 11, n. 1, article 1, 2015. doi:10.2168/lmcs-11(1:1)2015 (open access) (© the authors) //
  Conf. version in A. D. Gordon, ed., Proc. of 19th Europ. Symp. on Programming, ESOP 2010 (Paphos, March 2010), v. 6012 of Lect. Notes in Comput. Sci., pp. 488-506. Springer, 2010. doi:10.1007/978-3-642-11957-6_26 (© Springer) - pdf
• K. Nakata, T. Uustalu. Trace-based coinductive operational semantics for While: big-step and small-step, relational and functional styles.
  In S. Berghofer, T. Nipkow, C. Urban, M. Wenzel, eds., Proc. of 22nd Int. Conf. on Theorem Proving in Higher-Order Logics, TPHOLs 2009 (Munich, Aug. 2009), v. 5674 of Lect. Notes in Comput. Sci., pp. 375-390. Springer, 2009. doi:10.1007/978-3-642-03359-9_26 (© Springer) - pdf
• B. Fischer, A. Saabas, T. Uustalu. Program repair as sound optimization of broken programs.
  In Proc. of 3rd IEEE Int. Symp. on Theoretical Aspects of Software Engineering, TASE 2009 (Tianjin, July 2009), pp. 165-173. IEEE CS Press, 2009. doi:10.1109/tase.2009.61 (© IEEE) - pdf
• L. Pinto, T. Uustalu. Proof search and counter-model construction for bi-intuitionistic propositional logic with labelled sequents.
  In M. Giese, A. Waaler, eds., Proc. of 18th Int. Conf. on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2009 (Oslo, July 2009), v. 5607 of Lect. Notes in Artif. Intell., pp. 295-309. Springer, 2009. doi:10.1007/978-3-642-02716-1_22 (© Springer) - pdf
• M. J. Frade, A. Saabas, T. Uustalu. Bidirectional data-flow analyses, type-systematically.
  In Proc. of 2009 ACM SIGPLAN Wksh. on Partial Evaluation and Semantics-Based Program Manipulation, PEPM 2009 (Savannah, GA, Jan. 2009), pp. 141-149. ACM Press, 2009. doi:10.1145/1480945.1480965 (© ACM) - free pdf via ACM Author-Izer
• T. Uustalu, V. Vene. The recursion scheme from the cofree recursive comonad.
  Electron. Notes in Theor. Comput. Sci., v. 229, n. 5 (V. Capretta, C. McBride, eds., Proc. of 2nd Wksh. on Mathematically Structured Functional Programming, MSFP 2008, Reykjavík, July 2008), pp. 135-157, 2011. doi:10.1016/j.entcs.2011.02.020 (open access) (© Elsevier Science)
• V. Capretta, T. Uustalu, V. Vene. Corecursive algebras: a study of general corecursion.
  In M. Oliveira, J. Woodcock, eds., Revised Selected Papers from 12th Brazilian Symp. on Formal Methods, SBMF 2009 (Gramado, RS, Aug. 2009), v. 5902 of Lect. Notes in Comput. Sci., pp. 84-100. Springer, 2009. doi:10.1007/978-3-642-10452-7_7 (© Springer) - pdf
• A. Saabas, T. Uustalu. Proof optimization for partial redundancy elimination.
  J. of Log. and Algebraic Program., v. 78, n. 7, pp. 620-643, 2009. doi:10.1016/j.jlap.2009.05.002 (open access) (© Elsevier Science) //
  Conf. version in Proc. of 2008 ACM SIGPLAN Wksh. on Partial Evaluation and Semantics-Based Program Manipulation, PEPM 2008 (San Francisco, CA, Jan 2008), pp. 91-101. ACM Press, 2008. doi:10.1145/1328408.1328422 (© ACM) - free pdf via ACM Author-Izer (via ACM Author-Izer)
• T. Uustalu, V. Vene. Comonadic notions of computation.
  Electron. Notes in Theor. Comput. Sci., v. 203, n. 5 (J. Adámek, C. Kupke, eds., Proc. of 9th Int. Wksh. on Coalgebraic Methods in Computer Science, CMCS 2008, Budapest, Apr. 2008), pp. 263-284, 2008. doi:10.1016/j.entcs.2008.05.029 (open access) (© Elsevier Science)
• B. Jacobs, T. Uustalu. Semantics of grammars and attributes via initiality.
  In E. Barendsen, V. Capretta, H. Geuvers, M. Niqui, eds., Reflections on Type theory, Lambda-Calculus, and the Mind: Essays Dedicated to Henk Barendregt on the Occasion of His 60th Birthday, pp. 181-196. Radboud Univ. Nijmegen, 2007. article at publisher (open access)
• I. Hasuo, B. Jacobs, T. Uustalu. Categorical views on computations on trees.
  In L. Arge, C. Cachin, T. Jurdzinski, A. Tarlecki, eds., Proc. of 34th Int. Coll. on Automata, Languages and Programming, ICALP 2007 (Wroclaw, July 2007), v. 4596 of Lect. Notes in Comput. Sci., pp. 619-630. Springer, 2007. doi: 10.1007/978-3-540-73420-8_54 (© Springer) - pdf
• A. Saabas, T. Uustalu. Program and proof optimizations with type systems.
  J. of Log. and Algebraic Program., v. 77, n. 1-2, pp. 131-154, 2008. doi: 10.1016/j.jlap.2008.05.007 (open access) (© Elsevier Science)
• M. J. Frade, A. Saabas, T. Uustalu. Foundational certification of data-flow analyses.
  In Proc. of 1st IEEE and IFIP Int. Symp on Theor. Aspects of Software Engineering, TASE 2007 (Shanghai, June 2007), pp. 107-116. IEEE CS Press, 2007. doi: 10.1109/tase.2007.27 (© IEEE) - pdf
• A. Saabas, T. Uustalu. Type systems for optimizing stack-based code.
  Electron. Notes in Theor. Comput. Sci., v. 190, n. 1 (M. Huisman, F. Spoto, eds., Proc. of 2nd Wksh. on Bytecode Semantics, Verification, Analysis and Transformation, Bytecode 2007, Braga, March 2007), pp. 103-119, 2007. doi: 10.1016/j.entcs.2007.02.063 (open access) (© Elsevier Science)
• N. Ghani, M. Hamana, T. Uustalu, V. Vene. Representing cyclic structures as nested datatypes.
  In H. Nilsson, ed., Proc. of 7th Symp. on Trends in Functional Programming, TFP 2006 (Nottingham, Apr. 2006), pp. 173-188. Univ. of Nottingham, 2006. - pdf
• A. Saabas, T. Uustalu. Compositional type systems for stack-based low-level languages.
  Manuscript. - pdf //
  Conf. version in B. Jay, J. Gudmundsson, eds., Proc. of 12th Computing, Australasian Theory Symp., CATS 2006 (Hobart, Jan. 2006), v. 51 of Confs. in Research and Practice in Inf. Technol., pp. 27-39. Australian Comput. Soc., 2006. article in ACM DL (© Australian Comput. Soc.) - pdf
• T. Uustalu, V. Vene. Comonadic functional attribute evaluation.
  In M. van Eekelen, ed., Trends in Functional Programming 6, pp. 145-162. Intellect, 2007. book in Google Books - pdf //
  Conf. version in M. van Eekelen, ed., Proc. of 6th Symp. on Trends in Functional Programming, TFP '05 (Tallinn, Sept. 2005), pp. 33-43. Inst. of Cybern., 2005.
• P. Laud, T. Uustalu, V. Vene. Type systems equivalent to data-flow analyses for imperative languages.
  Theor. Comput. Sci., v. 364, n. 3, pp. 292-310, 2006. doi: 10.1016/j.tcs.2006.08.013 (open access) (© Elsevier Science) //
  Conf. version in M. Hofmann, H.-W. Loidl, eds., Proc. of 3rd APPSEM II Wksh., APPSEM '05 (Frauenchiemsee, Sept. 2005), 12 pp. Ludwig-Maximilians-Univ. München, 2005.
• A. Saabas, T. Uustalu. A compositional natural semantics and Hoare logic for low-level languages.
  Theor. Comput. Sci., v. 373, n. 3, pp. 273-302, 2007. doi: 10.1016/j.tcs.2006.12.020 (open access) (© Elsevier Science) //
  Conf. version in Electron. Notes in Theor. Comput. Sci., v. 156, n. 1 (P. D Mosses, I. Ulidowski, eds., Proc. of 2nd Wksh. on Structured Operational Semantics, SOS '05, Lisbon, July 2005), pp. 151-168, 2006. doi: 10.1016/j.entcs.2005.09.031 (open access) (© Elsevier Science)
• T. Uustalu, V. Vene. The essence of dataflow programming.
  In Z. Horváth, ed., Revised Selected Lectures from 1st Central European Functional Programming School, CEFP 2005 (Budapest, July 2005), v. 4164 of Lect. Notes in Comput. Sci., pp. 135-167. Springer, 2006. doi: 10.1007/11894100_5 (© Springer) - pdf //
  Short conf. version in K. Yi, ed., Proc. of 3rd Asian Symp. on Programming Languages and Systems, APLAS 2005 (Tsukuba, Nov. 2005), v. 3780 of Lect. Notes in Comput. Sci., pp. 2-18. Springer, 2005. doi: 10.1007/11575467_2 (© Springer) - pdf
• T. Uustalu, V. Vene. Signals and comonads.
  J. of Univ. Comput. Sci., v. 11, n. 7, pp. 1310-1326, 2005. doi: 10.3217/jucs-011-07-1311 (open access) (© J.UCS) //
  Conf. version in M. A. Musicante, R. M. F. Lima, eds., Proc. of 9th Brazilian Symp. on Programming Languages, SBLP '05 (Recife, PE, May 2005), pp. 215-228. Univ. de Pernambuco, Recife, 2005.
• N. Ghani, P. Johann, T. Uustalu, V. Vene. Monadic augment and generalised short cut fusion.
  Reprinted in ACM SIGPLAN Notices, v. 40, n. 9, pp. 294-305, 2005. doi: 10.1145/1090189.1086403 //
  In Proc. of 10th ACM SIGPLAN Int. Conf. on Functional Programming, ICFP '05 (Tallinn, Sept. 2005), pp. 294-305. ACM Press, 2005. doi: 10.1145/1086365.1086403 (© ACM) - free pdf via ACM Author-Izer
• N. Ghani, T. Uustalu, V. Vene. Generalizing the augment combinator.
  In H.-W. Loidl, ed., Trends in Functional Programming 5, pp. 65-78. Intellect, 2006. book in Google Books - pdf
• N. Ghani, T. Uustalu, V. Vene. Build, augment and destroy, universally.
  In W.-N. Chin, ed., Proc. of 2nd Asian Symp. on Programming Languages and Systems, APLAS 2004 (Taipei, Nov. 2004), v. 3302 of Lect. Notes in Comput. Sci., pp. 327-347. Springer, 2004. doi: 10.1007/978-3-540-30477-7_22 (© Springer) - pdf
• N. Ghani, T. Uustalu. Monad combinators, non-determinism and probabilistic choice (extended abstract).
  Manuscript, distributed at CMCIM 2004 (Copenhagen, Aug. 2004) - pdf
• V. Capretta, T. Uustalu, V. Vene. Recursive coalgebras from comonads.
  Inf. and Comput., v. 204, n. 4, pp. 437-468, 2006. doi: 10.1016/j.ic.2005.08.005 (open access) (© Elsevier Science) //
  Conf. version in Electron. Notes in Theor. Comput. Sci., v. 106 (J. Adámek, S. Milius, eds., Proc. of 7th Int. Wksh. on Coalgebraic Methods in Computer Science, CMCS '04, Barcelona, March 2004), pp. 43-61, 2004. doi: 10.1016/j.entcs.2004.02.034 (open access) (© Elsevier Science)
• T. Altenkirch, T. Uustalu. Normalization by evaluation for λ^→,2.
  In Y. Kameyama, P. J. Stuckey, eds., Proc. of 7th Int. Symp. on Functional and Logic Programming, FLOPS 2004 (Nara, Apr. 2004), v. 2998 of Lect. Notes. in Comput. Sci., pp. 260-275. Springer, 2004. doi: 10.1007/978-3-540-24754-8_19 (© Springer) - pdf
• N. Ghani, T. Uustalu, M. Hamana. Explicit substitutions and higher-order syntax.
  High.-Order and Symb. Comput., v. 19, n. 2-3, pp. 263-282, 2006. doi: 10.1007/s10990-006-8748-4 (© Springer) - pdf //
  Conf. version in F. Honsell, M. Miculan, A. Momigliano, eds., Proc. of 2nd ACM SIGPLAN Wksh. on Mechanized Reasoning about Languages with Variable Binding, MERλIN '03 (Uppsala, Aug. 2003), 7 pp. ACM Press, 2003. doi: 10.1145/976571.976580 (© ACM) - free pdf via ACM Author-Izer
• N. Ghani, T. Uustalu. Coproducts of ideal monads.
  Theor. Inf. and Appl., v. 38, n. 4, pp. 321-342, 2004. doi: 10.1051/ita:2004016 (© EDP Science) - free pdf from NUMDAM //
  Extended abstract in Z. Ésik, I. Walukiewicz, ed., Proc. of 5th Int. Wksh. on Fixed Points in Computer Science, FICS '03 (Warsaw, Apr. 2003), pp. 32-36. Warsaw Univ., 2003.
• T. Uustalu, V. Vene. An alternative characterization of complete iterativeness (extended abstract).
  In Z. Ésik, I. Walukiewicz, ed., Proc. of 5th Int. Wksh. on Fixed Points in Computer Science, FICS '03 (Warsaw, Apr. 2003), pp. 81-83. Warsaw Univ., 2003. - pdf
• R. Matthes, T. Uustalu. Substitution in non-wellfounded syntax with variable binding.
  Theor. Comput. Sci., v. 327, n. 1-2, pp. 155-174, 2004. doi: 10.1016/j.tcs.2004.07.025 (open access) (© Elsevier Science) //
  Conf. version in Electron. Notes in Theor. Comput. Sci., v. 82, n. 1 (H. P. Gumm, ed., Proc. of 6th Int. Wksh. on Coalgebraic Methods in Computer Science, CMCS '03, Warsaw, Apr. 2003), pp. 191-205, 2003. doi: 10.1016/s1571-0661(04)80639-x (open access) (© Elsevier Science)
• A. Abel, R. Matthes, T. Uustalu. Iteration schemes for higher-order and nested datatypes.
  Theor. Comput. Sci., v. 333, n. 1-2, pp. 3-66, 2005. doi: 10.1016/j.tcs.2004.10.017 (open access) (© Elsevier Science) //
  Conf. version Generalized iteration and coiteration for higher-order nested datatypes in A. D. Gordon, ed., Proc. of 6th Int. Conf. on Foundations of Software Science and Computation Structures, FoSSaCS 2003 (Warsaw, Apr. 2003), v. 2620 of Lect. Notes in Comput. Sci., pp. 54-69. Springer, 2003. doi: 10.1007/3-540-36576-1_4 (© Springer) - pdf
• T. Uustalu. Monad translating inductive and coinductive types.
  In H. Geuvers, F. Wiedijk, eds., Selected Papers from 2nd Int. Wksh. on Types for Proofs and Programs, TYPES 2002 (Berg en Dal, Apr. 2002), v. 2646 of Lect. Notes in Comput. Sci., pp. 299-315. Springer, 2003. doi: 10.1007/3-540-39185-1_17 (© Springer) - pdf
• T. Uustalu. Generalizing substitution.
  Theor. Inf. and Appl., v. 37, n. 4, pp. 315-336, 2003. doi: 10.1051/ita:2003022 (© EDP Sciences) - free pdf from NUMDAM //
  Extended abstract in Z. Ésik, A. Ingólfsdóttir, eds., Prel. Proc. of 4th Int. Wksh. on Fixed Points in Computer Science, FICS '02 (Copenhagen, July 2002), BRICS Notes Series NS-02-2, pp. 9-11. Dept. of Computer Science, Univ. of Aarhus, 2002.
• G. Barthe, T. Uustalu. CPS translating inductive and coinductive types (extended abstract).
  Reprinted in ACM SIGPLAN Notices, v. 37, n. 3, pp. 131-142, 2002. doi: 10.1145/509799.503043 //
  In Proc. of 2002 ACM SIGPLAN Wksh. on Partial Evaluation and Semantics-Based Program Manipulation, PEPM '02 (Portland, OR, Jan. 2002), pp. 131-142. ACM Press, 2002. doi: 10.1145/503032.503043 (© ACM) - free pdf via ACM Author-Izer
• T. Uustalu. (Co)monads from inductive and coinductive types.
  In L. M. Pereira, P. Quaresma, eds., Proc. of 2001 APPIA-GULP-PRODE Joint Conf. on Declarative Programming, AGP '01 (Évora, Sept. 2001), pp. 47-61. Univ. de Évora, 2001. - pdf
• T. Uustalu, V. Vene. The dual of substitution is redecoration.
  In K. Hammond, S. Curtis, eds, Trends in Functional Programming 3, pp. 99-110. Intellect, Bristol / Portland, OR, 2002. book in Google Books - pdf
• T. Uustalu, V. Vene, A. Pardo. Recursion schemes from comonads.
  Nordic J. of Computing, v. 8, n. 3, pp. 366-390, 2001. (© Publ. Assoc. Nordic J. of Computing) - pdf
• G. Barthe, M. J. Frade, E. Giménez, L. Pinto, T. Uustalu. Type-based termination of recursive definitions.
  Math. Struct. in Comput. Sci., v. 14, n. 1, pp. 97-141, 2004. doi: 10.1017/s0960129503004122 (© Cambridge Univ. Press) - pdf
• T. Uustalu, V. Vene. Coding recursion à la Mendler (extended abstract).
  In J. Jeuring, ed., Proc. of 2nd Wksh. on Generic Programming, WGP 2000 (Ponte de Lima, July 2000), Techn. Report UU-CS-2000-19, pp. 69-85. Dept. of Comput. Sci., Univ. Utrecht, 2000. - pdf
• T. Uustalu, V. Vene. Mendler-style inductive types, categorically.
  Nordic J. of Computing, v. 6, n. 3, pp. 343-361, 1999. (© Publ. Assoc. Nordic J. of Computing) - pdf
• T. Uustalu. Multi-(co)iteration, categorically.
  In J. Penjam, ed., Proc. of 6th Fenno-Ugric Symp. on Software Technology, FUSST '99 (Sagadi, Aug. 1999), Report CS 104/99, pp. 259-267. Inst. of Cybernetics, 1999. - pdf
• T. Uustalu, V. Vene. Primitive (co)recursion and course-of-value (co)iteration, categorically.
  Informatica, v. 10, n. 1, pp. 5-26, 1999. doi: 10.3233/inf-1999-10102, article at publisher (open access) (© Inst. of Math. and Inf.)
• V. Vene, T. Uustalu. Functional programming with apomorphisms (corecursion).
  Proc. of Estonian Acad. of Sci.: Phys., Math., v. 47, n. 3, pp. 147-161, 1998. issue in Google Books (© Estonian Academy Publishers) - pdf
• T. Uustalu, V. Vene. Least and greatest fixed-points in intuitionistic natural deduction.
  Theor. Comput. Sci., v. 272, n. 1-2, pp. 315-339, 2002. doi: 10.1016/s0304-3975(00)00355-8 (open access) (© Elsevier Science)
• T. Uustalu. Natural deduction for intuitionistic least and greatest fixedpoint logics, with an application to program construction.
  PhD thesis, Diss. TRITA-IT AVH 98:03, Dept. of Teleinformatics, Royal Inst. of Technol., Stockholm, 1998.
• T. Uustalu, V. Vene. A cube of proof systems for the intuitionistic predicate μ,ν-logic.
  In M. Haveraaen, O. Owe, eds., Selected Papers from 8th Nordic Wksh. on Programming Theory, NWPT '96 (Oslo, Dec. 1996), Research Report 248, pp. 237-246. Inst. for informatikk, Univ. i Oslo, 1997. - pdf
• T. Uustalu. Aspects of structural synthesis of programs.
  Lic thesis, Research Report TRITA-IT R 95:09, Dept. of Teleinformatics, Royal Inst. of Technol., Stockholm, 1995.
• B. Mayoh, E. Tyugu, T. Uustalu. Constraint satisfaction and constraint programming: a brief lead-in.
  In B. Mayoh, E. Tyugu, J. Penjam, eds., Proc. of NATO ASI on Constraint Programming (Pärnu, Aug. 1993), v. 131 of NATO ASI Series F, pp. 1-16. Springer, 1994. doi: 10.1007/978-3-642-85983-0_1 (© Springer)
• E. Tyugu, T. Uustalu. Higher-order functional constraint networks.
  In B. Mayoh, E. Tyugu, J. Penjam, eds., Proc. of NATO ASI on Constraint Programming (Pärnu, Aug. 1993), v. 131 of NATO ASI Series F, pp. 116-139. Springer, 1994. doi: 10.1007/978-3-642-85983-0_5 (© Springer)
• T. Uustalu. Combining object-oriented and logic paradigms: a modal logic programming approach.
  In O. Lehrmann Madsen, ed., Proc. of 6th Europ. Conf. on Object-Oriented Programming, ECOOP '92 (Utrect, June/July 1992), v. 615 of Lect. Notes in Comput. Sci., pp. 98-113. Springer, 1992. doi: 10.1007/bfb0053032 (© Springer) - pdf
• T. Uustalu. Combination of object-oriented and logic paradigms.
  MSc thesis, Tallinn Techn. Univ., 1992. (Written at Norwegian Inst. of Technol., Trondheim, 1991.) - pdf
• T. Uustalu, P. Lorents. On some classes of hereditarily r.e. sets.
  Proc. of Estonian Acad. Sci.: Phys., Math., v. 39, n. 2, pp. 108-112, 1990. (In Russian.) (© Estonian Academy Publishers) - pdf
• T. Uustalu, M. Pentus. Sequent systems of modal calculi.
  Preprint. Inst. of Cybernetics, 1989. (In Russian.) (© Estonian Academy Publishers) - pdf
• T. Uustalu. On recursive functionals of higher types.
  In Abstracts of Conf. on Theoretical and Applied Questions in Mathematics (Tartu, Sept. 1985), v. 1, pp. 188-190. Univ. of Tartu, 1985. (In Russian.) - pdf