Abstract:

Logic and semantics are important tools in computer science. For instance, they allow us to verify both large computer programs and large proofs. In our EU-STREP project we computer verified exact numerical computations using type theory to tightly connect reasoning and computation. Fields medalist Voevodsky has proposed type theory as a new foundation for mathematics more suitable for computer verification. In the past years, we have taken this foundation to create a framework better suited for program verification. Finally, I will show how we apply these ideas in high assurance cryptography.

Bio:

Bas is Associate Professor in the logic and semantics group at Aarhus University. He holds a PhD in mathematics from Nijmegen University. He has been awarded an elite veni grant by the Dutch funding agency NWO. 

He is co-author of the book on univalent foundations and of the accompanying library of computer proofs.  He's been a member of 26 program committees. He has held positions in Nijmegen, Chalmers, Paris-Sud, CMU and was a member of the Institute for Advanced Study in Princeton. He is currently funded on a three year project Guarded Homotopy Type Theory by the Villum foundation which he obtained joint with Lars Birkedal.