Iosif Petrakis

foto,  March 6, 2017
Position
Temporary Assistant Professor
Academic sector
MATH-01/A - Mathematical Logic
Research sector (ERC-2024)
PE1_1 - Logic and foundations

PE1_17 - Mathematical aspects of computer science

Office
Ca' Vignal 2,  Floor 2,  Room 1
Telephone
+39 045 802 7973
E-mail
iosif|petrakis*univr|it <== Replace | with . and * with @ to have the right email address.

Office Hours

Tuesday, Hours 3:00 PM - 5:00 PM,   Ca' Vignal 2, Floor 2, room 1

Curriculum

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

Modules running in the period selected: 3.
Click on the module to see the timetable and course details.

Di seguito sono elencati gli eventi e gli insegnamenti di Terza Missione collegati al docente:

  • Eventi di Terza Missione: eventi di Public Engagement e Formazione Continua.
  • Insegnamenti di Terza Missione: insegnamenti che fanno parte di Corsi di Studio come Corsi di formazione continua, Corsi di perfezionamento e aggiornamento professionale, Corsi di perfezionamento, Master e Scuole di specializzazione.
Research interests
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



Organization

Department facilities

Share