# 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: