Curriculum Vitae
Last updated: January 2024
Research Interests
Category Theory | Type Theory | Constructive Logic & Mathematics | Categorical Logic & Topos Theory | Homotopy Type Theory | Applied Category Theory | Programming Language Theory | Automated Reasoning & Formal Verification
Publications
“Parametricity via Cohesion,” accepted to MFPS 2024, proceedings to appear in ENTICS, preprint available on arXiv: https://arxiv.org/abs/2404.03825
“Foundations of Substructural Dependent Type Theory,” preprint available on arXiv: https://arxiv.org/abs/2401.15258
Education & work experience
PhD Pure & Applied Logic, Computer Science Department, Carnegie Mellon University (2023-present)
BA Computer Science & Philosophy, Merton College, University of Oxford (2018-2023)
- Graduated with First Class Honors
- Ranked 1st in upper-level exams out of cohort of students in all undergraduate Computer Science degrees at Oxford
- Academic awards:
- University of Oxford Department of Computer Science: Gibbs Prize for Preliminary Examinations in Computer Science and Philosophy, paying particular regard to Computer Science papers (2018-2019)
- Merton College: Exhibition scholarship for outstanding academic performance (awarded 2019, renewed 2020)
- Merton College: Postmaster scholarship in recognition of sustained academic excellence (promoted from Exhibition in 2021)
- Merton College: Summer Projects Scheme undergraduate research grant (awarded 2020, see “research experience & grants” below)
- University of Oxford Department of Computer Science Gibbs Prize for Computer Science and Philosophy – Parts A and B Computer Science papers (2022-2023)
- University of Oxford Department of Computer Science Gibbs Prize for Computer Science and Philosophy – Part A and B Philosophy papers (2022-2023)
- University of Oxford Department of Computer Science Gibbs Prize for Computer Science/Mathematics and Computer Science/Computer Science and Philosophy – Parts A and B best overall performance (2022-2023)
Primary & secondary education, freelance work: I was homeschooled part-time from the age of 6, and then full-time from the age of 10, due to me being far enough ahead of my grade level in school that skipping grades was infeasible. At 14, I had completed the equivalent of a high-school education, and chose to pursue a career in music as a freelance composer. At the age of 20, however, spurred by newfound interests in programming, logic, and the foundations of mathematics and computer science, I became determined to study these subjects at a research level. Applying to universities posed a challenge given my background, as I lacked a high-school diploma and most other qualifications expected for an undergraduate application, but by 2018 I had successfully applied and been admitted to the University of Oxford, where I studied for five years, and was subsequently admitted to my current position as a PhD student at CMU.
Research Experience & Grants
Undergraduate research project: Church Encodings in Higher-Dimensional Type Theory – Toward a Theory of Abstraction (2020)
- Independent research project funded by grant from the Merton Summer Projects Scheme: https://www.merton.ox.ac.uk/news/new-york-nightclubbing-and-laser-accelerators-college-funds-10-student-summer-projects
- Investigated combining constructs from cubical type theory for the type-theoretic treatment of propositional equality with modalities from quantitative type theory (as defined by Abel, Atkey, and McBride) for tracking usage of computational resources.
- Demonstrated the ability to internally prove parametricity theorems and derive induction principles for Church-encoded datatypes in a type theory combining cubical and quantitative methods.
- Supervisor: Luke Ong
- Project report submitted to Merton College available at:
https://www.merton.ox.ac.uk/sites/default/files/inline-files/Aberle%2C%20Connor_0.pdf
Skills & Interests
Programming/IT: I am proficient at programming in Agda, Haskell, OCaml, Common Lisp, Scala, and C, as well as typesetting technical documents in LaTeX, including complicated diagrams arising in category theory, automata theory, etc. I designed my website www.cbaberle.com from scratch.
Music: music composition and theory remain passions from my pre-university years, and I am keenly interested in applications of computer science and mathematics to problems of analysis and expression in music and the arts more generally; a sampling of my musical work can be found on my website at: www.cbaberle.com/music