Publications

Note

My thesis contains cleaned up and extended versions of the papers "Tait in one big step", "Big step normalisation" and "Type theory should eat itself". I suggest you look in the thesis instead of reading the original papers.

Relative monads formalised

with Thorsten Altenkirch and Tarmo Uustalu

Accepted for publication in the Journal of Formalized Reasoning. Final version pending.

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. ISBN?

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. ISBN?

Also publised in ACM SIGPLAN Notices, to appear.

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.