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

We study the following topics:

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

- 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

- Danel Ahman (U. of Ljubljana)
- Flavien Breuvart (LIPN)
- Sergey Goncharov (FAU Erlangen-Nürnberg)
- Renato Neves (INESC Tec, U. do Minho)
- Exequiel Rivas (U. Nacional de Rosario / Tallinn UT)
- Niccolň Veltri (Tallinn UT)
- Niels Voorneveld (Tallinn UT)

- Sergey Goncharov, FAU Erlangen-Nürnberg → RU, 26 March-4 Apr. 2019
- Exequiel Rivas, Inria Paris → RU, 26 Apr.-4 May 2019
- Maciej Piróg, U. of Wroclaw → RU, 28 Nov.-2 Dec. 2019
- Renato Neves, U. do Minho → RU, 1-8 Dec. 2019
- 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, 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 UT, 12-20 Dec. 2021

- 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

**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, 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 [pdf]**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*, article 6, 14 pp. ACM Press, 2020. doi:10.1145/3414080.3414084 [pdf]**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 [pdf]**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 Software Science and Computation Structures, FoSSaCS 2022 (Munich, Apr. 2022)*,*Lect. Notes in Comput. Sci.*, Springer, to appear.**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 (Lódz, March 2022)*,*Electron. Proc. in Theor. Comput. Sci.*, Open Publishing Assoc., to appear.

- 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 Topos Inst. 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
- 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, 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
- N. Veltri, Deductive systems for categories with skew structure, 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
- 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]

Tarmo Uustalu

Last update 2 January 2022