CS Colloquium - Bas Spitters: Modern Type Theory and Secure Blockchains
Types help programmers to write clear and correct programs. I will present recent developments in type theory which will allow us to write bigger libraries and address new areas of computer science.
Info about event
Time
Location
Building 5510, room 104 (Incuba Lille Aud)
This is part of a big international research program to connect programming, logic and mathematics. As part of this program we collaboratively wrote a 500pp book and used type theory to check the mathematical proofs.
One important application of type theory is to help create secure blockchains and smart contracts. To do this we need to check the mathematical proofs used in cryptography and reason about the programs and programming languages used for blockchains.
I will give a high level overview of the work in my group. Our work spans a spectrum in computer science, ranging from mathematics to engineering. I have joined projects with both departments within the DIGIT center.
My work is supported by AFOSR and the Concordium foundation.
Inaugural lecture
Bas came to the department as a visiting associate professor in 2015 on an AUFF grant. Together with Lars Birkedal, he was then awarded a 3.3 Mkr Villum grant: Guarded Homotopy Type Theory. In autumn 2018 he was hired into a permanent associate professor position.