Computer Laboratory

Ian Orton


Programming, Logic, and Semantics Group
Cambridge Computer Lab
Room: FC07
Email: ian.orton [at] cl.cam.ac.uk

Research

Currently a PhD student under Prof Andrew Pitts. Interested in models of homotopy type theory and type theory in general.

Lately I have been working on (models of) type theories with an interval object such as cubical type theory. See these slides for more information.

Papers

  • Axioms for Modelling Cubical Type Theory in a Topos, I. Orton and A. M. Pitts, CSL 2016. [Paper] [Agda]

Research Talks

  • Axioms for Modelling Cubical Type Theory in a Topos, Workshop on HoTT/UF, Toronto, May 2016. [Slides]
  • Modelling Cubical Type Theory in Agda, Workshop on HoTT/UF, Porto, June 2016. [Slides]
  • Axioms for Modelling Cubical Type Theory in a Topos, Logic Colloquium, Leeds, August 2016. [Slides]

Misc

  • Verified Programming in Agda, PhD Students' Lecture Series, 2017 [Slides]

Teaching

This year (2016/17) I am supervising:

I have prevously supervised: