Quantified computational effects and interaction

This is a research project funded by the Icelandic Research Fund, run at the Department of Computer Science of Reykjavik University from Jan. 2019 to Dec. 2021 (extended until Aug. 2022).

Research programme

We study the following topics:

• graded monads and monad-like objects,
• graded distributive laws,
• interaction laws of monads and monad-like objects.

People

Participants

• Tarmo Uustalu, PI
• Shin-ya Katsumata (NII, Tokyo), co-PI
• Maciej Piróg (U. of Wroclaw), co-PI


• Dylan McDermott, postdoc
• Yasuaki Morita, PhD student
• Ülo Reimaa (U. of Tartu), guest postdoc

Collaborators

• Danel Ahman (U. of Ljubljana)
• Flavien Breuvart (LIPN)
• Sergey Goncharov (FAU Erlangen-Nürnberg)
• Renato Neves (INESC Tec and U. do Minho)
• Exequiel Rivas (Inria Paris, then UN Rosario)
• Niccolò Veltri (Tallinn UT)
• Niels Voorneveld (Tallinn UT)

Project activity

Research and conference visits

• Tarmo Uustalu, RU → Xitou (IFIP WG 2.1 #78), 16-23 March 2019
• Sergey Goncharov, FAU Erlangen-Nürnberg → RU, 26 March-4 Apr. 2019 (paid by FAU Erlangen-Nürnberg)
• Exequiel Rivas, Inria Paris → RU, 26 Apr.-4 May 2019
• Tarmo Uustalu, RU → London (CALCO/MFPS '19), 3-7 June 2019
• Tarmo Uustalu, RU → Amsterdam (CONCUR '19), 25-31 Aug. 2019 (funded by T.U.'s RU research grant)
• Tarmo Uustalu, RU → LIPN, U. Sorbonne Paris Nord, 16-30 Sept. 2019 (paid by LIPN)
• Maciej Piróg, U. of Wroclaw → RU, 28 Nov.-2 Dec. 2019
• Renato Neves, U. do Minho → RU, 1-8 Dec. 2019
• Tarmo Uustalu, RU → Otterlo (IFIP WG 2.1 #79), 5-8 Jan. 2020 (funded by T.U.'s RU research grant)
• Shin-ya Katsumata, NII Tokyo → RU, 26 Jan.-6 Feb. 2020
• Ülo Reimaa, U. of Tartu → RU, 31 Jan.-15 March 2020
• Dylan McDermott, RU → U. of Cambridge, 2-4 Feb. 2020
• Niccolò Veltri, Tallinn UT → RU, 16-21 Feb. 2020 (paid by Tallinn UT)
• Niels Voorneveld, Tallinn UT → RU, 10-15 March 2020 (paid by Tallinn UT)
• Exequiel Rivas, Inria Paris → RU, 18-29 Aug. 2020
• Tarmo Uustalu, RU → U. of Wroclaw, 23-31 Aug. 2021
• Dylan McDermott, RU → U. of Wroclaw and Tallinn UT (incl. PPDP '21), 24 Aug.-13 Sept. 2021
• Yasuaki Morita, RU → Tallinn UT, 4-18 Oct. 2021
• Niels Voorneveld, Tallinn UT → RU, 29 Oct.-12 Nov. 2021 (paid by Tallinn UT)
• Dylan McDermott, RU → Tallinn (SYCO-8), 12-20 Dec. 2021
• Tarmo Uustalu, RU → Łódź (NCL '22), 13-18 March 2022 (funded by T.U.'s RU research grant)
• Dylan McDermott, RU → München (ETAPS '22), 1-7 Apr. 2022
• Tarmo Uustalu, RU → München (ETAPS '22), 1-5 Apr. 2022 (funded by T.U.'s RU research grant)
• Dylan McDermott, RU → Brno (PSSL-106), 13-18 May 2022 (funded partially by T.U.'s RU research grant)

Talks of visitors at RU

• S. Goncharov, Guarded traced categories for recursion and iteration (joint work with L. Schröder, P. B. Levy), talk at ICE-TCS seminar, RU, 2 Apr. 2019
• E. Rivas, Effects and monads: merging operators (joint work with M. Jaskelioff), keynote talk at ICE-TCS Theory Day, RU, 3 May 2019
• M. Piróg, Equational theories and monads from polynomial Cayley representations (joint work with P. Polesiuk, F. Sieczkowski), talk at ICE-TCS seminar, RU, 29 Nov. 2019
• S. Katsumata, Differentiable causal computations via delayed trace (joint work with D. Sprunger), talk at ICE-TCS seminar, RU, 27 Jan. 2020
• N. Veltri, Formalizing pi-calculus in Guarded Cubical Agda (joint work with A. Vezzosi), talk at ICE-TCS seminar, RU, 17 Feb. 2020
• N. Voorneveld, Inductive and coinductive predicate liftings for effectful programs (joint work with N. Veltri), talk at ICE-TCS seminar, RU, 8 Nov. 2021

Results and dissemination

Articles

• 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., art. 14, 19 pp. Dagstuhl Publishing, 2019. doi:10.4230/lipics.calco.2019.14
• S. Katsumata, E. Rivas, T. Uustalu. Interaction laws of monads and comonads. 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 [copy]
• D. McDermott, M. Piróg, T. Uustalu. Degrading lists. In Proc. of 22nd Int. Symp. on Principles and Practice of Declarative Languages, PPDP 2020 (Bologna, Sept. 2020), ACM Int. Conf. Proc. Series, art. 6, 14 pp. ACM Press, 2020. doi:10.1145/3414080.3414084 [postprint in Opin vísindi]
• T. Uustalu, N. Veltri, N. Zeilberger. Eilenberg-Kelly reloaded. Electron. Notes in Theor. Comput. Sci., v. 352 (P. Johann, ed., Proc. of 36th Conf. on Mathematical Foundations of Programming Semantics, MFPS XXXVI, Paris, June 2020), pp. 233-256, 2020. doi:10.1016/j.entcs.2020.09.012
• T. Uustalu, N. Veltri, N. Zeilberger. Proof theory of partially normal skew monoidal categories. In D. I. Spivak, J. Vicary, eds., Proc. of 3rd Ann. Int. Applied Category Theory Conf., ACT 2020 (Cambridge, MA, July 2020), v. 333 of Electron. Proc. in Theor. Comput. Sci., pp. 230-246. Open Publishing Assoc., 2021. doi:10.4204/eptcs.333.16
• 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), v. 12470 of Lect. Notes in Comput. Sci., pp. 186-205. Springer, 2020. doi:10.1007/978-3-030-64437-6_10 [postprint in Opin vísindi]
• T. Uustalu, N. Veltri, N. Zeilberger. Deductive systems and coherence for skew prounital closed categories. In C. Sacerdoti Coen, A. Tiu, eds., Proc. of 15th Int. Wksh. on Logical Frameworks and Metalanguages: Theory and Practice, LFMTP 2020 (Paris, June 2020), v. 332 of Electron. Proc. in Theor. Comput. Sci., pp. 35-53. Open Publishing Assoc., 2021. doi:10.4204/eptcs.332.3
• N. Arkor, D. McDermott. Abstract clones for abstract syntax. In N. Kobayashi, ed., Proc. of 6th Int. Conf. on Formal Structures for Computation and Deduction, FSCD 2021 (Buenos Aires, July 2021), v. 195 of Leibniz Int. Proc. in Inform., art. 30, 19 pp. Dagstuhl Publishing, 2021. doi:10.4230/lipics.fscd.2021.30
• D. McDermott, E. Rivas, T. Uustalu. Sweedler theory of monads. In P. Bouyer, L. Schröder, eds., Proc. of 25th Int. Conf. on Foundations of Software Science and Computation Structures, FoSSaCS 2022 (Munich, Apr. 2022), v. 13242 of Lect. Notes in Comput. Sci., pp. 428-448. Springer, 2022. doi:10.1007/978-3-030-99253-8_22
• T. Uustalu, N. Veltri, C.-S. Wan. Proof theory of skew non-commutative MILL. In A. Indrzejczak, M. Zawidzki, eds., Proc. of 10th Int. Conf. on Non-classical Logics: Theory and Applications, NCL '22 (Łódź, March 2022), v. 358 of Electron. Proc. in Theor. Comput. Sci., pp. 118-135. Open Publishing Assoc., 2022. doi:10.4204/eptcs.358.9
• D. McDermott, T. Uustalu. What makes a strong monad? In J. Gibbons, M. S. New, eds., Proc. of 9th Wksh. on Mathematically Structured Functional Programming, MSFP 2022 (Munich, Apr. 2022), v. 360 of Electron Proc. in Theor. Comput. Sci., pp. 113-133. Open Publishing Assoc., 2022. doi:10.4204/eptcs.360.6
• D. McDermott, A. Mycroft. Galois connecting call-by-value and call-by-name. In A. Felty, ed., Proc. of 7th Int. Conf. on Formal Structures for Computation and Deduction, FSCD 2022 (Haifa, Aug. 2022), v. 228 of Leibniz Int. Proc. in Inform., art. 32, 19 pp. Dagstuhl Publishing, 2022. doi:10.4230/lipics.fscd.2022.32
• D. McDermott, T. Uustalu. Flexibly graded monads and graded algebras. In E. Komendantskaya, ed., Proc. of 14th Int. Conf. on Mathematics of Program Construction, MPC 2022 (Tbilisi, Sept. 2022), v. 13544 of Lect. Notes in Comput. Sci., pp. 102-128. Springer, 2022. doi:10.1007/978-3-031-16912-0_4 [postprint in Opin vísindi]
• S. Katsumata, D. McDermott, T. Uustalu, N. Wu. Flexible presentations of graded monads. Proc. of ACM on Program. Lang., v. 6, n. ICFP (Proc. of 27th ACM SIGPLAN Int. Conf. on Functional Programming, ICFP '22, Ljubljana, Sept. 2022), art. 123, 29 pp., 2022. doi:10.1145/3547654
• F. Breuvart, D. McDermott, T. Uustalu. Canonical gradings of monads. In J. Master, M. Lewis, eds., Proc. of 5th Int. Conf. on Applied Category Theory, ACT 2022 (Glasgow, July 2022), v. 380 of Electron. Proc. in Theor Comput. Sci., pp. 1-21. Open Publishing Assoc., 2023. doi:10.4204/eptcs.380.1
• D. McDermott, Y. Morita, T. Uustalu. A type system with subtyping for WebAssembly's stack polymorphism. In H. Seidl, Z. Liu, C. S. Pasareanu, eds., Proc. of 19th Int. Coll. on Theoretical Aspects of Computing, ICTAC 2022 (Tbilisi, Sept. 2022), v. 13572 of Lect. Notes in Comput. Sci., pp. 305-323. Springer, 2022. doi:10.1007/978-3-031-17715-6_20 [postprint in Opin vísindi]

Talks

• T. Uustalu, The functional programming revolution, talk at UTmessan, Reykjavik, 8 Feb. 2019 [video]
• T. Uustalu, Decomposing comonad morphisms (joint work with D. Ahman), talk at CALCO 2019, London, 3-6 June 2019
• T. Uustalu, Concurrent monads of resumptions and traces, talk at RADICAL 2019, Amsterdam, 26 Aug. 2019
• T. Uustalu, Resumption monads for shared-memory concurrency, talk at Joint Estonian-Latvian Theory Days in Pärnu, 11-13 Oct. 2019
• D. McDermott, On the relation between call-by-value and call-by-name (joint work with A. Mycroft), talk at ICE-TCS seminar, RU, 4 Nov. 2019
• T. Uustalu, Monad-comonad interaction laws (joint work with S. Katsumata, E. Rivas), talk at IFIP WG 2.1 meeting #79, Otterlo, 6-10 Jan. 2020
• T. Uustalu, Ultrasubstructural logics (joint work with N. Veltri, N. Zeilberger), talk at ICE-TCS seminar, RU, 24 Feb. 2020
• N. Veltri, Skew everything! diving deep under substructural logics (joint work with T. Uustalu, N. Zeilberger), talk at CS Theory Seminar, Tallinn UT, 27 Feb. 2020
• N. Veltri. Eilenberg-Kelly reloaded (joint work with T. Uustalu, N. Zeilberger), talk at MFPS 2020, Paris, online, 2-5 June 2020 [video]
• D. McDermott, Higher-order algebraic theories (joint work with N. Arkor), talk at CS Theory Seminar, Tallinn UT, online, 4 June 2020
• T. Uustalu, Interaction laws of monads and comonads (joint work with S. Katsumata, E. Rivas), talk at seminar of Chair of Geometric Methods in Mathematics, TU Dresden, online, 12 June 2020
• T. Uustalu, Interaction laws of monads and comonads (joint work with S. Katsumata, E. Rivas), talk at CS Theory seminar, Tallinn UT, online, 2 July 2020
• N. Veltri, Proof theory of partially normal skew monoidal categories (joint work with T. Uustalu, N. Zeilberger), talk at ACT 2020, Cambridge, MA, online, 6-10 July 2020, [video]
• E. Rivas, Interaction laws of monads and comonads (joint work with S. Katsumata, T. Uustalu), talk at LICS 2020, Saarbrücken, online, 8-11 July 2020 [video]
• T. Uustalu, Interaction laws of monads and comonads (joint work with S. Katsumata, E. Rivas), talk at OWLS seminar, online, 29 July 2020 [video]
• N. Voorneveld, Merging coeffect production into effect handling (joint work with T. Uustalu), talk at HOPE 2020, Jersey City, NJ, online, 23 Aug. 2020 [video]
• D. McDermott, Degrading lists (joint work with M. Piróg, T. Uustalu), talk at PPDP 2020, Bologna, online, 8-10 Sept. 2020
• E. Rivas, Interaction laws of monads and comonads (joint work with S. Katsumata, T. Uustalu), talk at LoVE seminar, LIPN, online, 15 Oct. 2020
• T. Uustalu, Monad-comonad interaction laws, monad algebras, comonad coalgebras (joint work with S. Katsumata, E. Rivas, N. Voorneveld), talk at MIT Categories Seminar, online, 22 Oct. 2020 [video]
• N. Voorneveld, Algebraic and coalgebraic perspectives on interaction laws (joint work with T. Uustalu), talk at APLAS 2020, Fukuoka, online, 30 Nov.-2 Dec. 2020 [video]
• N. Zeilberger, Skew monoidal categories and the proof-theoretic anatomy of associativity (joint work with T. Uustalu, N. Veltri), talk at Mathematical Foundations Seminar, U. of Bath, online, 9 Feb. 2021
• T. Uustalu, Skew X categories and structural proof theory (joint work with N. Veltri, N. Zeilberger), talk at CCS Colloquium, Augusta U., online, 26 Feb. 2021 [video]
• N. Veltri, Proof theory of skew monoidal categories (joint work with T. Uustalu, N. Zeilberger), talk at seminar of Proofs and Algorithms Pole, LIX, online, 15 March 2021 [video]
• T. Uustalu, Polynomial comonads, talk at Wksh. on Polynomial Functors, online, 15-19 March 2021 [video]
• T. Uustalu, Skew X categories and structural proof theory (joint work with N. Veltri, N. Zeilberger), talk at seminar of Centro de Matemática, U. do Minho, online, 25 March 2021
• T. Uustalu, Monads and interaction, course at MGS 2021, Sheffield, online, 12-16 Apr. 2021 [course material]
• N. Zeilberger, Skew monoidal categories and the proof-theoretic anatomy of associativity (joint work with T. Uustalu, N. Veltri), Mathematical Foundations Seminar, talk at CS Theory Seminar, Tallinn UT, online, 13 May 2021
• N. Arkor, Higher-order algebraic theories and relative monads (joint work with D. McDermott), talk at Masaryk U. Algebra Seminar, Brno, online, 13 May 2021 [video]
• N. Arkor, Higher-order algebraic theories and relative monads (joint work with D. McDermott), talk at Categories and Companions Symp. 2021, online, 8-12 June 2021 [video]
• N. Zeilberger, Skew monoidal categories and the proof-theoretic anatomy of associativity (joint work with T. Uustalu, N. Veltri), talk at Masaryk U. Algebra Seminar, online, 10 June 2021 [video]
• T. Uustalu, Monad-comonad interaction laws (co)algebraically (joint work with D. McDermott, S. Katsumata, E. Rivas, N. Voorneveld), talk at BIRS Workshop "Tangent Categories and Their Applications"/FMCS 2021, Banff, AB, online, 14-18 June 2021 [video]
• T. Uustalu, Monads and interaction, course at OPLSS 2021, Eugene, OR, online, 14-26 June 2021
• N. Arkor, Abstract clones for abstract syntax (joint work with D. McDermott), talk at FSCD 2021, Buenos Aires, online, 19-22 July 2021 [video]
• D. McDermott, E. Rivas, T. Uustalu, Interaction laws of monads and comonads, tutorial at ICFP 2021, Daejon, online, 22-27 Aug. 2021 [tutorial material]
• N. Veltri, Deductive systems for categories with skew structure (joint work with T. Uustalu, N. Zeilberger), talk at special session of MFPS XXXVII, Salzburg, online, 30 Aug.-2 Sept. 2021 [video]
• N. Arkor, The formal theory of theories (first half joint work with Dylan McDermott), talk at CT 20→21, Genoa, 30 Aug.-4 Sept. 2021 [video]
• D. McDermott, List monads (joint work with M. Piróg, T. Uustalu), talk at CS Theory Seminar, Tallinn UT, 3 Sept. 2021 [video]
• Y. Morita, A type system with subtyping for WebAssembly's stack polymorphism (joint work with D. McDermott, T. Uustalu), talk at CS Theory Seminar, Tallinn UT, 14 October 2021
• T. Uustalu, List monads (joint work with D. McDermott, M. Piróg), talk at seminar of Proofs and Algorithms Pole, LIX, online, 18 Oct. 2021 [video]
• T. Uustalu, List monads (joint work with D. McDermott, M. Piróg), invited talk at Scottish Programming Languages Seminar (SPLS), St. Andrews, online, 20 Oct. 2021 [video]
• T. Uustalu, List monads (joint work with D. McDermott, M. Piróg), talk at IFIP WG 2.1 short online meeting, 26 Oct. 2021
• Y. Morita, A type system with subtyping for WebAssembly's stack polymorphism (joint work with D. McDermott, T. Uustalu), talk at NWPT '21, Reykjavik, 4-6 Nov. 2021
• N. Arkor, The (relative) monad - theory correspondence (joint work with D. McDermott), talk at CS Theory Seminar, Tallinn UT, online, 11 Nov. 2021
• D. McDermott, On the relation between call-by-value and call-by-name (joint work with A. Mycroft), talk at SYCO-8, Tallinn, 13-14 Dec. 2021
• D. McDermott, Flexible presentations of graded monads (joint work with S. Katsumata, T. Uustalu, N. Wu), talk at CS Theory Seminar, Tallinn UT, 17 Dec. 2021 [video]
• C.-S. Wan, Proof theory of skew non-commutative MILL (joint work with T. Uustalu, N. Veltri), talk at World Logic Day 2022 Logic in Estonia Workshop, online, 14 Jan. 2022
• C.-S. Wan, Proof theory of skew non-commutative MILL (joint work with T. Uustalu, N. Veltri), talk at NCL 2022, Łódź, 14-18 March 2022
• N. Arkor, The (relative) monad - theory correspondence (joint work with D. McDermott), Masaryk U. Algebra Seminar, 17 March 2022 [video]
• D. McDermott, What makes a strong monad? (joint work with T. Uustalu), talk at MSFP 2022, Munich, 2 Apr. 2022 [video]
• D. McDermott, Sweedler theory of monads (joint work with E. Rivas, T. Uustalu), talk at FoSSaCS 2022, Munich, 4-7 Apr. 2022
• D. McDermott, Flexible presentations of graded monads (joint work with S. Katsumata, T. Uustalu, N. Wu), talk at U. of Strathclyde MSP 101 seminar, online, 21 Apr. 2022 [video]
• T. Uustalu, Logics of skew categorical structures (joint work with N. Veltri, C.-S. Wan), talk at Logic4Peace, online, 22-23 Apr. 2022
• T. Uustalu, What it takes (mathematically) to run effectful computations? (based on joint work with D. McDermott, S. Katsumata, E. Rivas, N. Voorneveld), talk at Copenhagen Programming Languages Seminar (COPLAS), online, 26 Apr. 2022
• T. Uustalu, What makes a strong monad? (joint work with D. McDermott), talk at IFIP WG 2.1 short online meeting, online, 27 Apr. 2022
• T. Uustalu, List monads (joint work with D. McDermott, M. Piróg), talk at Estonian-Latvian Theory Days in Riga, 6-8 May 2022
• S. Capobianco, Additive cellular automata monadically (joint work with T. Uustalu), talk at Estonian-Latvian Theory Days in Riga, 6-8 May 2022
• C.-S. Wan, Proof theory of skew non-commutative MILL (joint work with T. Uustalu, N. Veltri), talk at Estonian-Latvian Theory Days in Riga, 6-8 May 2022
• D. McDermott, Higher-order algebraic theories (joint work with N. Arkor), talk at seminar of Proofs and Algorithms Pole, LIX, online, 9 May 2022
• D. McDermott, Flexible presentations of graded monads (joint work with S. Katsumata, T. Uustalu, N. Wu), talk at PSSL-106, Brno, 14-15 May 2022
• Y. Morita, A type system with subtyping for WebAssembly's stack polymorphism (joint work with D. McDermott, T. Uustalu), talk at PAW 2022, Berlin, 6 June 2022
• D. McDermott, Canonical gradings of monads (joint work with F. Breuvart, T. Uustalu), talk at Meeting on Graded Types, U. of Kent, Canterbury, 17 June 2022 [video]
• D. McDermott, Flexible presentations of graded monads (joint work with S. Katsumata, T. Uustalu, N. Wu), talk at TYPES 2022, Nantes, 20-23 June 2022 [video]
• T. Uustalu, Monad-comonad interaction laws (based on joint work with S. Katsumata, D. McDermott, E. Rivas), invited talk at CLA 2022, Tallinn, 20-22 June 2022 [video]
• T. Uustalu, Programming-language thinking, talk at a seminar at Guardtime AS, Tallinn, 20 June 2022 [video]
• C.-S. Wan, Proof theory of skew non-commutative MILL (joint work with T. Uustalu, N. Veltri), talk at Logic Colloquium, Reykjavik, 27 June-1 July 2022
• D. McDermott, Canonical gradings of monads (joint work with F. Breuvart, T. Uustalu), talk at ACT 2022, Glasgow, 18-22 July 2022 [video]
• D. McDermott, Galois connecting call-by-value and call-by-name (joint work with A. Mycroft), talk at FSCD 2022, Haifa, 2-5 Aug. 2022
• D. McDermott, Flexibly graded monads and graded algebras (joint work with T. Uustalu), talk at HOPE 2022, Ljubljana, 11 Sept. 2022 [video]
• D. McDermott, Flexible presentations of graded monads (joint work with S. Katsumata, T. Uustalu, N. Wu), talk at ICFP 2022, Ljubljana, 12-14 Sept. 2022 [video]
• D. McDermott, Flexibly graded monads and graded algebras (joint work with T. Uustalu), talk at MPC 2022, Tbilisi, 26-28 Sept. 2022 [video]
• Y. Morita, A type system with subtyping for WebAssembly's stack polymorphism (joint work with D. McDermott, T. Uustalu), talk at ICTAC 2022, Tbilisi, 27-30 Sept. 2022