James Chapman

When is a container a comonad?

with Danel Ahman and Tarmo Uustalu

In Logical Methods in Computer Science 10 (3). September 3, 2014.

Relative Monads Formalised

with Thorsten Altenkirch and Tarmo Uustalu

In Journal of Formalized Reasoning 7 (1) 2014.

Normalization by Evaluation in the Delay Monad

A Case Study for Coinduction via Copatterns and Sized Types

with Andreas Abel

In Paul Levy and Neel Krishnaswami: Proceedings 5th Workshop on Mathematically Structured Functional Programming (MSFP 2014), Grenoble, France, 12 April 2014, Electronic Proceedings in Theoretical Computer Science, 153, pp. 55-67

Dependently Typed Programming in Agda

with Ulf Norell

Online version

MSFP 2012 Proceedings

editors James Chapman and Paul Blain Levy

Proceedings of Fourth Worshop on Mathematically Structured functional Programming (MSFP 2012). Tallinn, March 2012. EPTCS.

When is a container a comonad?

with Danel Ahman and Tarmo Uustalu

In L. Birkedal, ed., Proc. of 15th Int. Conf. on Foundations of Software Science and Computation Structures, FoSSaCS 2012 (Tallinn, March 2012), Lect. Notes in Comput. Sci., Springer.

MSFP 2010 Proceedings

editors Venanzio Capretta and James Chapman

Proceedings of 3rd ACM SIGPLAN Worshop on Mathematically Structured functional Programming (MSFP 2010). Baltimore, September 2010. ACM Press.

The Gentle Art of Levitation

with Pierre-Evariste Dagand, Conor McBride and Peter Morris

In proceedings of 15th ACM SIGPLAN International Conference on Functional Programming, (ICFP '10). Baltimore, September 2010. pages 3--14. ACM Press.

Also publised in ACM SIGPLAN Notices.

Monads need not be endofunctors

with Thorsten Altenkirch and Tarmo Uustalu

In proceedings of 13th International Conference on Foundations of Software Science and Computational Structures (FoSSaCS), Paphos, Cyprus, March 2010. Volume 6014 Lecture Notes in Computer Science, Springer. ISBN 978-3-642-12031-2.

Machine assisted proofs in the theory of monads

with Thorsten Altenkirch and Tarmo Uustalu

In proceedings of Nordic Workshop on Programming Theory (NWPT), Copenhagen, Denmark, October 2009.

Big step normalisation

with Thorsten Altenkirch

In Journal of Functional Programming 19 (3 & 4) May 2009. Special Issue on Mathematically Structured Functional Programming (MSFP 2006). Cambridge University Press. (extended/refined version in my PhD thesis).

Type checking and normalisation

PhD Thesis. Examiners: Thierry Coquand and Venanzio Capretta. Submitted 30th October 2008. Defended 13th January 2009.

Type theory should eat itself

In proceedings of International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), Pittsburg, Pennsylvania, June 2008. Electronic Notes in Theoretical Computer Science No. 228. Elsevier. (extended/refined version in my PhD thesis).

Tait in one big step

with Thorsten Altenkirch

In proceedings of Workshop on Mathematically Structured Functional Programming, Kuressaare, Estonia, July 2nd, 2006. Electronic Workshop in Computing (eWiC). British Computer Society. (extended/refined version in my PhD thesis).

Epigram Reloaded

with Thorsten Altenkirch and Conor McBride

In Revised and Selected Papers from the Sixth Symposium on Trends in Functional Programming, Tallinn, Estonia, 2005. Trends in Functional Programming 6 Intellect 2007, ISBN 978-1-84150-176-5.