Daniël Otten
I am a PhD candidate at the University of Amsterdam, interested in type theory and category theory.
I am a PhD candidate at the University of Amsterdam, interested in type theory and category theory.
I am a PhD candidate at the University of Amsterdam, part of the Institute for Logic, Language, and Computation, and member of the Mathematical and Computational Logic Unit. My supervisors are Benno van den Berg and Herman Geuvers.
My main interest is type theory, which I study using tools from category theory. A central objective is proving conservativity results: showing that minimalistic versions of type theory can already derive the same statements as more complex versions. These results allows for flexibility: simple versions are easier to model and study, while more extensive versions are convenient to work in and therefore implemented by proof assistents. An example of such a result is our paper: Conservativity of Type Theory over Higher-order Arithmetic. Other interests include: higher-order logic, constructive mathematics, cyclic proofs, proof assistants, and homotopy theory.
Office F1.22C
Science Park 107
1098 XG Amsterdam
The Netherlands