Sean Moss
<sean.moss@univ.ox.ac.uk>
I am a Senior Research Associate at the Department of Computer Science, University of Oxford, working with Sam Staton. From October 2017 to September 2021 I was a Junior Research Fellow in Computer Science at University College, Oxford. Previously I was a PhD student of Martin Hyland at the University of Cambridge.
Research
My mathematical and computer science interests include:
- Category theory: topos theory, categorical logic, fibred categories.
- Dependent type theory and its semantics, homotopy theory.
- Programming language theory: computational effects, probabilistic programming, local state, full abstraction.
I also work with Philipp Koralus at the Faculty of Philosophy on a content-based theory of human cognitive capacity for reasoning and decision-making. The idea is to make precise the hypothesis that resolving questions is central to how the mind works. A book is forthcoming.
Publications
- C. Matache, S. Moss, and S. Staton. Recursion and Sequentiality in Categories of Sheaves. Proceedings of 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). doi:10.4230/LIPIcs.FSCD.2021.25. Preprint: arXiv:2105.02156.
- S. Moss. Another approach to the Kan–Quillen model structure. Journal of Homotopy and Related Structures, vol 15, 2020. doi:10.1007/s40062-019-00247-y. Preprint: arXiv:1506.04887.
- A. Ścibior, O. Kammar, M. Vákár, S. Staton, H. Yang, Y. Cai, K. Ostermann, S.K. Moss, C. Heunen, and Z. Ghahramani. Denotational validation of Bayesian inference. Proceedings of 45th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2018). doi:10.1145/3158148. Preprint: arXiv:1711.03219.
- S.K. Moss and T. von Glehn. Dialectica models of type theory. Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018). doi:10.1145/3209108.3209207. Preprint: arXiv:2105.00283.
- O. Kammar, P.B. Levy, S.K. Moss, and S. Staton. A monad for full ground reference cells. Proceedings of 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017). doi:10.1109/LICS.2017.8005109. Preprint: arXiv:1702.04908.
Thesis
The Dialectica Models of Type Theory. University of Cambridge. doi:10.17863/CAM.28036.
Teaching
- In Hilary term 2020 I lectured Lambda Calculus and Types.
- Since 2017 in Oxford I have given tutorials in the CS undergraduate courses Logic and Proof and Functional Programming.
- Between 2013-2017 in Cambridge I gave supervisions in the CS undergraduate course Denotational Semantics and in the Mathematics undergraduate courses Groups, Numbers and Sets, Logic and Set Theory, Algebraic Topology, and Number Fields. I also gave examples classes in Part III (MMath) Category Theory.