Sean Moss

Junior Research Fellow in MPLS (Computer Science)

Research

My research interests are in category theory and its applications to type theory and programming language theory. A type theory is any of a wide family of formal languages which capture the both the notion of proof in mathematics and the practice of computer programming. Category theory originated in mathematics as the study of the structure of the entire collection of mathematical objects of some type, but it turns out that categories can also be used to give meaning to a type theory. I primarily study type theories via this categorical semantics, which allows one to use machinery and intuition from pure mathematics to gain a better understanding of the nature of proof and programming.

Selected Publications

Sean Moss, Another approach to the Kan-Quillen model structure, arXiv:1506.04887

Ohad Kammar, Paul B. Levy, Sean K. Moss, Sam Staton, A monad for full ground reference cells, 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)