Herman Geuvers

Proofs for programs and programs for proofs: a case for dependent types.

Abstract: In programming languages, types give a partial specification and help the programmer in avoiding mistakes. But if we use dependent types, we can express a full specification of a program using its type. Then programming becomes finding a term of a specific type. Following the Curry-Howard formulas-as-types embedding, we can view dependent types as formulas, and finding a term for a type is then the same as finding a proof of a formula. In the last decade, dependent type theory has thus become a integrated system for programming and proving. The proof assistant Coq supports this: a user can write programs and prove these correct, but also write proofs and extract (correct) programs from these. In the talk we will show how dependent type theory works, showing some concrete examples in Coq, and we will discuss the limitations and challenges of the approach.

Bio: Herman Geuvers (1964) is professor in Theoretical Informatics at the Radboud University Nijmegen (since 2006) and in Proving with Computer Assistance at the Eindhoven University of Technology (since 2007). He has studied mathematics in Nijmegen and wrote his PhD thesis in the Foundations of Computer Science under supervision of Henk Barendregt (Nijmegen 1993) on the Curry-Howard formulas-as-types interpretation that relates logic and type theory. He has given many courses at the Radboud University Nijmegen and the Eindhoven University of Technology, mainly on topics such as logic, theoretical computer science, type theory, semantics of programming languages. Also he has been a lecturer in Type Theory at various international PhD summer schools. His research is in type theory, proof assistants and formalizing mathematics. He has been a member of various program committees and has been the organizer of various scientific events. Moreover, he has been the co-editor of the book Selected Papers on Automath (see above). He has supervised a number of PhD projects in the area of type theory, logic, proof assistants and formalizing mathematics, and has received various research grants in this research field (both at the national and EU level). He has been the leader of the ”FTA project” at the Radboud University Nijmegen, to formalize a constructive proof of the Fundamental Theorem of Algebra in Coq. This has led to CoRN, the Coq Repository of formalized mathematics at Nijmegen, being a large library of formalized algebra and analysis by means of the proof assistant Coq, which is continuously under development