# 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]
- Axioms for Univalence, I. Orton and A. M. Pitts, TYPES 2017. [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: