Computational effects and high-level control (CTRL-F)

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

Research programme

We study the following topics:

• computational effects and iteration (infinite computations),
• computational effects and concurrency,
• computational effects and event-drivenness.

People

Participants

• Tarmo Uustalu, PI
• Sergey Goncharov (FAU Erlangen-Nürnberg), co-PI
• Renato Neves (U. do Minho), co-PI
• Exequiel Rivas (Marigold / Tallinn UT), co-PI


• Dylan McDermott, postdoc
• Yasuaki Morita, PhD student
• Basile Gros (ENSEEIHT), intern (guest MSc student)

Project activity

Research and conference visits

• Yasuaki Morita, RU → Berlin (ECOOP '22), 5-10 June 2022
• Dylan McDermott, RU → U. of Kent, Canterbury (Mtg. on Graded Types) and L2SN, U. Nantes (TYPES '22), 16-23 June 2022
• Exequiel Rivas, Milan → Tallinn UT, 11-18 July 2022
• Dylan McDermott, RU → U. of Strathclyde, Glasgow (ACT '22), 17-22(24) July 2022
• Dylan McDermott, RU → Technion, Haifa (FLoC '22), (29 July)1-7 Aug 2022
• José Espírito Santo and Luís Pinto, U. do Minho, Braga → RU, 26 Aug.-4 Sept. 2022 (paid by ICE-TCS)
• Dylan McDermott, RU → Ljubljana (ICFP '22), (8)9-15 Sept. 2022
• Dylan McDermott, RU → Tbilisi (CLAS '22), 23-30 Sept. 2022
• Yasuaki Morita, RU → Tbilisi (CLAS '22), 23-30 Sept. 2022
• Nathanael Arkor, Masaryk U., Brno → RU, 4-25 Nov. 2022 (paid by ICE-TCS)
• Sergey Goncharov, FAU Erlangen-Nürnberg → RU, 8-15 Jan. 2023
• Maciej Piróg, Standard Chartered → Palaiseau (CLA '23), 11-14 Jan. 2023
• Denis Firsov, Guardtime and Tallinn UT → RU, 1-10 March 2023 (not paid by the project)
• Ülo Reimaa, U of Tartu → RU, 15 March-2 Apr. 2023
• Tarmo Uustalu, RU → FAU Erlangen-Nürnberg, 17-21 Apr. 2023
• Patrik Eklund, U of Umeå → RU, 14-17 May 2023 (not paid by the project)
• Dylan McDermott, RU → Tallinn UT, 17-29 May 2023
• Shin-ya Katsumata, NII, Tokyo → RU, 31 May-10 June 2023
• Maciej Piróg, Standard Chartered → RU, 13-18 June 2023
• Flavien Breuvart, U Sorbonne Paris Nord → (9)23 Aug.-4 Oct. 2023

Talks of visitors at RU

• J. Espírito Santo, Russell-Prawitz translation and atomic polymorphism (joint work with G. Ferreira), talk at ICE-TCS seminar, 1 Sept. 2022
• L. Pinto, Coinductive proof search for intuitionistic propositional logic (joint work with J. Espírito Santo, R. Matthes), talk at ICE-TCS seminar, 1 Sept. 2022
• N. Arkor, A 2-dimensional perspective on polymorphism, talk at ICE-TCS seminar, 7 Nov. 2022
• S. Goncharov, Towards a higher-order mathematical operational semantics (joint work with S. Milius, L. Schröder, S. Tsampas, H. Urbat), talk at ICE-TCS seminar, 12 Jan. 2023
• D. Firsov, EasyCrypt for working cryptographers, talk at ICE-TCS seminar, 9 March 2023
• Ü. Reimaa, Introduction to cocategories, talk at ICE-TCS seminar, 27 March 2023

Results and dissemination

Papers

• 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 [copy]
• 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 M. Lewis, J. Master, eds., Proc. of 5th Ann. Int. Applied Category Theory Conf., ACT 2022 (Glasgow, July 2022), Electron. Proc. in Theor Comput. Sci., Open Publishing Assoc., to appear. article at publisher

Manuscripts

• E. Rivas. A proposal for procontainers from computational effects. Latest version May 2022.
• D. McDermott, A. Mycroft. Galois connecting call-by-value and call-by-name. Latest version Feb. 2023. arXiv 2202.08246 [cs.PL]
• N. Arkor, D. McDermott. The formal theory of relative monads. Latest version May 2023. arXiv 2302.14014 [math.CT]
• N. Arkor, D. McDermott. Relative monadicity. Latest version May 2023. arXiv 2305.10405 [math.CT]

Talks

• 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]
• 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]
• T. Winterhalter, Verifying non-terminating programs with IO in F^* (joint work with C.-C. Andrici, C. Hritcu, E. Rivas), 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
• T. Uustalu, Skewness everywhere, talk at Types, Thorsten and Theories: Thorsten Altenkirch's 60th birthday celebration, Nottingham, 12 Oct. 2022 [video]
• T. Uustalu, Additive cellular automata graded-monadically (joint work with S. Capobianco), talk at IFIP WG 2.1 short online meeting, 24 Oct. 2022
• N. Arkor, Relative monads and their many guises (joint work with D. McDermott), talk at Category Theory Octoberfest 2022, online, 29-30 Oct. 2022 [video]
• T. Uustalu, Additive cellular automata graded-monadically (joint work with S. Capobianco), talk at Comonad meetup, online, 16 Oct. 2022
• M. Piróg, Counting monads on lists, talk at 16th Wksh. on Computational Logic and Applications (joint work with D. McDermott, T. Uustalu), talk at CLA '23, Palaiseau near Paris, 12-13 Jan. 2023
• E. Rivas, Procontainers and computational effects, talk at 2^o Encontro Brasileiro em Teoria das Categorias, São Paulo, SP, 20-24 March 2023
• N. Arkor, The formal theory of relative monads (joint work with D. McDermott), talk at PSSL-107, Athens, 1-2 Apr. 2023
• T. Uustalu, Additive cellular automata graded-monadically (joint work with S. Capobianco), talk at Oberseminar Theoretische Informatik, FAU Erlangen-Nürnberg, 18 April 2023