# Research Interests Category Theory | Type Theory | Automated Reasoning | Program Synthesis | Formal Verification | Constructive Logic & Mathematics | Categorical Logic & Topos Theory | Homotopy Type Theory | Applied Category Theory | Programming Language Theory # Publications **[[Substructural Parametricity]],** joint work with Frank Pfenning Chris Martens, and Karl Crary. FSCD 2025. arXiv: [2503.03153](https://arxiv.org/abs/2503.03153) **[[Polynomial Universes in Homotopy Type Theory]],** joint work with David Spivak. arXiv: [2409.19176](https://arxiv.org/abs/2409.19176) **[[Parametricity via Cohesion]],** MFPS 2024. arXiv: [2404.03825](https://arxiv.org/abs/2404.03825) # Talks **[[Synthetic Mathematics, Logical Frameworks, and Categorical Algebra]],** talk given at the Topos Institute Berkeley Seminar during my time as Summer RA in 2025. video: [https://youtu.be/MjkWT6GkISI](https://youtu.be/MjkWT6GkISI) **[[Fundamental Theorems for Free]],** talk given at the CMU HoTT Seminar in January 2025. video: [https://youtu.be/wzBnOd00hcg](https://youtu.be/wzBnOd00hcg) **[[All Concepts are Essentially Algebraic]],** talk given at the Topos Institute Berkeley Seminar during my time as Summer RA in 2024. video: [https://youtu.be/RmiTOa4b0bA](https://youtu.be/RmiTOa4b0bA) # Preprints **[[Composing in Code]],** preprint of research on learnability of a custom embedded domain-specific language for symbolic music by large language models, done for my final project for a class on generative AI for music, taken at CMU in Fall 2025. url: [https://cbaberle.com/Preprints/Composing+in+Code](https://cbaberle.com/Preprints/Composing+in+Code) **[[Compositional Program Verification with Polynomial Functors in Agda]],** preprint of research based on ideas from my time working as a Summer RA at the Topos Institute in 2024 and 2025. url: [https://cbaberle.com/Preprints/Compositional+Program+Verification+with+Polynomial+Functors+in+Agda](https://cbaberle.com/Preprints/Compositional+Program+Verification+with+Polynomial+Functors+in+Agda) **[[Double Orthogonal Factorization Systems]],** joint work with Elena Caviglia, Matt Kukla, Ruben Maldonado, Luca Mesiti, Dorette Pronk, and Tanjona Ralaivosaona as part of the ACT 2024 Adjoint School. arXiv: [2509.26343](https://arxiv.org/abs/2509.26343) **"Foundations of Substructural Dependent Type Theory,"** preprint available on arXiv: [https://arxiv.org/abs/2401.15258](https://arxiv.org/abs/2401.15258) # Software **The Hyrax Project:** an Agda library/personal wiki/digital garden focusing on synthetic mathematics, written in literate Agda: [https://hyrax.cbaberle.com/index.html](https://hyrax.cbaberle.com/index.html) # Teaching **Categorical Logic, CMU, Spring 2026** — Instructor, along with Kian Cho and Owen Milner **Types and Programming Languages, CMU, Fall 2024** — TA for Jan Hoffmann (instructor) # Research & Work Experience **Topos Institute Summer 2025 Research Associate:** * May-August 2025 * Worked with Evan Patterson and Kevin Carlson on Double Theories and Simplicial Algebraic Theories, with input from Dana Scott on Agda formalization. **Topos Institute Summer 2024 Research Associate:** * June-August 2024 * Worked with David Spivak on Polynomial Functors and Natural Models of Dependent Type Theory * Topos Institute Blog Post on Summer 2024 Research Associates available at: [https://topos.site/blog/2024-07-29-summer-research-associates-2024/](https://topos.site/blog/2024-07-29-summer-research-associates-2024/) **Applied Category Theory Adjoint School 2024:** * Participated in research group on properties of double fibrations led by Dorette Pronk. * Wrote blog post **Prismatic Category Theory** for the n-Category Café on Grothendieck fibrations, joint work with Rubén Maldonado, available at: [https://golem.ph.utexas.edu/category/2024/08/prismatic_category_theory.html](https://golem.ph.utexas.edu/category/2024/08/prismatic_category_theory.html) * Developed Agda library for Simplicial Type Theory for use in formalizing our group's results. * Presentation of research at Applied Category Theory 2024, video available at: [https://www.youtube.com/watch?v=OaWgSWPCQeE](https://www.youtube.com/watch?v=OaWgSWPCQeE) **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](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:<br> [https://www.merton.ox.ac.uk/sites/default/files/inline-files/Aberle%2C%20Connor_0.pdf](https://www.merton.ox.ac.uk/sites/default/files/inline-files/Aberle%2C%20Connor_0.pdf) # Education **PhD Pure & Applied Logic, Computer Science Department, Carnegie Mellon University** (2023-present) * **Advisor:** Frank Pfenning * **Anticipated Graduation:** June 2028 **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 academic acceleration, completing the equivalent of a high-school education by 14, at which point I 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. --- # Skills & Interests **Programming/IT:** I am proficient at programming in Agda, Haskell, OCaml, C, Python, and Lisp-family languages such as Common Lisp and Scheme/Racket, as well as typesetting technical documents in LaTeX, including complicated diagrams arising in category theory, automata theory, etc. **Philosophy:** about half of my undergraduate work was in philosophy (concentrating on logic, philosophy of mathematics, and philosophy of science), and I remain keenly interested in philosophical issues pertaining to science, mathematics, the arts, and ethics, which I have continued to read and write about on occasion in my spare time. A sampling of my philosophical writing is available on my website. **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 output is available on my website.