Book · in preparation
Symmetry
With Marc Bezem, Ulrik Buchholtz, Bjørn Ian Dundas and Daniel R. Grayson. Group theory, rebuilt on the symmetries that univalent foundations gives to every type.
Assistant Professor · Computer Science
Pierre Cagne
I work on the foundations of mathematics and of computer science: univalent mathematics, the semantics of data types, and categorical logic.
About
I am an assistant professor (tenure-track) in the Department of Computer Science at Appalachian State University, in Boone, North Carolina. Before that, I was a postdoctoral researcher at Appalachian State, at Aarhus University in Denmark, and at the University of Bergen in Norway.
My research sits between theoretical computer science and the foundations of mathematics. The topics I keep coming back to:
- categorical logic
- homotopical algebra
- topos theory
- univalent mathematics
- dependent type theory
- data types
- proof assistants
- verified mathematics
I am one of the authors of Symmetry, a book that develops group theory and its offshoots directly in univalent mathematics.
I received my PhD in December 2018 from Université Paris Diderot (now Université Paris Cité), under the joint supervision of Paul-André Melliès (IRIF) and Clemens Berger (Laboratoire J.A. Dieudonné, Nice). More on my research page and in my CV.
Selected work
LICS 2024
On symmetries of spheres in univalent foundations
The symmetries of the circle form two copies of the circle. For higher spheres there are still two components, each with fundamental group ℤ/2ℤ.
MSCS 2024
GADTs are not (even partial) functors
A semantics of GADTs that extends the usual semantics of algebraic data types must contain ghost elements, and those break parametricity.
Contact
- cagnep@appstate.edu
- Office
- 308-C Anne Belk Hall
- Department of Computer Science
Appalachian State University
224 Joyce Lawrence Lane
Boone, NC 28608, USA - Elsewhere
- ORCID · arXiv