La ricerca di Petrakis riguarda la matematica costruttiva, la teoria della computabilità e la teoria delle categorie. Si è occupato principalmente di topologia costruttiva e teoria della misura e, negli ultimi anni, delle connessioni tra la teoria degli insiemi di Bishop, la teoria dei tipi di Martin Loef e la teoria delle categorie. Petrakis ha pubblicato su riviste di logica e informatica teorica (tra cui Annals of Pure and Applied Logic, Computability, Journal of Logic and Analysis, Journal of Logic and Computation, Logical Methods in Computer Science, Mathematical Structures in Computer Science, Theoretical Computer Science) , nel Handbook of Constructive Mathematics e negli atti di convegni (inclusi 6 CiE, 2 LFCS, 1 LICS, 1 TYPES).
Modules running in the period selected: 3.
Click on the module to see the timetable and course details.
Course | Name | Total credits | Online | Teacher credits | Modules offered by this teacher |
---|---|---|---|---|---|
Bachelor's degree in Computer Science | Algebra and Foundations of Mathematics [Matricole pari] (2024/2025) | 6 | 6 | ||
Master's degree in Computer Science and Engineering | Interactive Theorem Proving (2023/2024) | 6 | 6 | ||
Master's degree in Mathematics | Advanced course in foundations of mathematics (2016/2017) | 6 | 6 |
Di seguito sono elencati gli eventi e gli insegnamenti di Terza Missione collegati al docente:
Topic | Description | Research area |
---|---|---|
Type Theory and Category Theory | 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. |
Algebra, Geometry, and Mathematical Logic
Mathematical logic and foundations |
Proof theory and constructive mathematics | 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. |
Algebra, Geometry, and Mathematical Logic
Mathematical logic and foundations |
Office | Collegial Body |
---|---|
member | Computer Science Teaching Committee - Department Computer Science |
member | Computer Science Department Council - Department Computer Science |
******** CSS e script comuni siti DOL - frase 9957 ********p>