# 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