-

People with expertise in this area
Research interests

Iosif Petrakis: Temporary Assistant Professor

Peter Michael Schuster: Full Professor

Research interests
Topic	People	Description
Hilbert's Programme for Abstract Mathematics	Peter Michael Schuster	Extracting the computational content of classical proofs in conceptual mathematics. Particular attention is paid to invocations of logical completeness in mathematical form, typically as variants of Zorn's Lemma.
Type Theory and Category Theory	Iosif Petrakis	Martin Loef Type Theory is a foundational framework both for functional programming and constructive mathematics. Its recent extension, Homotopy Type Theory, revealed new, unexpected connections between algebraic topology and theoretical computer science. Certain categorical models of dependent types generate the, so-called, dependent category theory, and its dual, codependent category theory.
Proof theory and constructive mathematics	Iosif Petrakis Peter Michael Schuster	Proof theory at large studies mathematical proofs, which thus become themselves objects of mathematics. In a nutshell, the goal is to understand "what can be proved with what" and to gain computational information from proofs. Constructive mathematics aims at direct proofs from which one can read off algorithms; any such algorithm comes with a certificate of correctness for free, which just is the original proof.