Formalizing restriction categoriesChapman, James; Uustalu, Tarmo; Veltri, NiccoloJournal of formalized reasoning2017 / p. 1-36 https://doi.org/10.6092/issn.1972-5787/6237

Machine assisted proofs in the theory of monadsAltenkirch, Thorsten; Chapman, James; Uustalu, Tarmo21st Nordic Workshop on Programming Theory : NWPT 2009 : Lyngby, Denmark, 14-16 October 2009 : proceedings2009 / p. 83-85 https://jmchapman.io/papers/Assisted_Monads.pdf

Monads need not be endofunctorsAltenkirch, Thorsten; Chapman, James; Uustalu, TarmoLogical methods in computer science2015 / p. 1-40 http://dx.doi.org/10.2168/LMCS-11(1:3)2015

Quotienting the delay monad by weak bisimilarityChapman, James; Uustalu, Tarmo; Veltri, NiccoloMathematical structures in computer science2019 / p. 67-92 https://doi.org/10.1017/s0960129517000184 Journal metrics at Scopus Article at Scopus Journal metrics at WOS Article at WOS

Quotienting the delay monad by weak bisimilarityChapman, James; Uustalu, Tarmo; Veltri, Niccolo21st International Conference on Types for Proofs and Programs, TYPES 2015 : Tallinn, Estonia, 18-21 May 2015 : abstracts2015 / p. 38-39

Relative monads formalisedAltenkirch, Thorsten; Chapman, James; Uustalu, TarmoJournal of formalized reasoning2014 / p. 1-43

A type-theoretical study of nontermination = Tüübiteoreetiline uurimus mittetermineeruvusestVeltri, Niccolo2017 https://digi.lib.ttu.ee/i/?7631

When is a container a comonad?Ahman, Danel; Chapman, James; Uustalu, TarmoFoundations of Software Science and Computational Structures : 15th International Conference, FOSSACS 2012, Held as Part of The European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012 : proceedings2012 / p. 74-88 : ill https://artiklid.elnet.ee/record=b2491247*est

When is a container a comonad?Ahman, Danel; Chapman, James; Uustalu, TarmoLogical methods in computer science2014 / p. 1-48 : ill