Contemporary · a field of logic
Cutting-Edge Research
Reverse mathematics, proof mining, homotopy type theory, descriptive complexity: where the field is being written now.
- The problem
- Exactly which axioms does a given theorem need, and can foundations themselves be made computational?
- The turning point
- The univalence axiom: equivalent structures are equal, making homotopy type theory a computational foundation.
- An open question
- Will univalent foundations, reverse mathematics, and proof mining reshape what we take “foundations” to mean?
The Canon
- Homotopy Type Theory 2013
- Subsystems of Second Order Arithmetic
- Applied Proof Theory
To study it
- Descriptive Complexity