Unexpectedly this is how you and I meet!
I was a master student at Radboud in Nijmegen. I like both math and computer science! I was very lucky and got to work on my thesis with Robbert Krebbers and Jules Jacobs. The thesis’ topic was verifying incorrectness in the Coq proof assistant. Here is the abstract
Incorrectness Separation Logic is a formal framework for local reasoning about the presence of bugs. Because of its foundations in formal methods Incorrectness Sepa- ration Logic comes with a “no false positive” soundness theorem. The soundness of this proof system relates proof derivation and true bugs. Thanks to this approach, static tools for bug finding can be thought as proof finders. We present a strongest- postcondition like calculus that allow us to verify incorrectness specifications as Separation Logic assertions the same way the weakest-precondition has been used to verify correctness specifications as Separation Logic assertions. We also provide a mechanization of Incorrectness Separation Logic in the Coq proof assistant using this strongest-postcondition like calculus.
Most of my time is spent on the internet and studying, sort of.
I like to experiment with programming languages from time to time and I read too much about programming and software. I really like interactive environments, starting with LISP and Scheme down to UNIX but by day I study mostly programming language semantics, type theory or some mathematics.
Who knows 🤷! My crystal ball is broken 🔮🔨!
I have finished my master! Thanks to everybody, I could not have made it withouth you all.
I finally managed to get into one of those ambigous masters in which you study something from math and something from computer science. It’s called Mathematical Foundations of Computer Science, AKA MFOCS.
I really enjoyed discovering new course such as computability theory but the most fun has been proof assistants.