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.

Papers

  • Axioms for Modelling Cubical Type Theory in a Topos, I. Orton and A. M. Pitts, CSL 2016. [Paper] [Agda] [Expanded version]
  • Models of Type Theory Based on Moore Paths, I. Orton and A. M. Pitts, FSCD 2017. [Paper]
  • Axioms for Univalence, I. Orton and A. M. Pitts, TYPES 2017. [Paper] [Agda]
  • Decomposing the Univalence Axiom, I. Orton and A. M. Pitts, arXiv preprint. A significantly expanded version of "Axioms for Univalence". [Paper]
  • Internal Universes in Models of Homotopy Type Theory, D. R. Licata, I. Orton, A. M. Pitts, B. Spitters, arXiv preprint. [Paper]

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]
  • Axioms for Univalence, TYPES 2017, Budapest, May 2017. [Slides]

Misc

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

Teaching

This year (2017/18) I am supervising:

I have prevously supervised: