Post-doc at INRIA/IRIF/Université Paris Cité. I mostly try to convince proof assistants that they are doing reasonable things. Sometimes this involves studying type theory. Sometimes this means understanding what our implementations do. All in all, it's not too bad. Profile banner (from the Leonard comic by Turk & de Groot): - I wanted to serve science because it it my joy and instead of that, what am I doing?... - Yes, what is he doing? - I guess he's complaining!
Post-doc at INRIA/IRIF/Université Paris Cité. I mostly try to convince proof assistants that they are doing reasonable things. Sometimes this involves studying type theory. Sometimes this means understanding what our implementations do. All in all, it's not too bad. Profile banner (from the Leonard comic by Turk & de Groot): - I wanted to serve science because it it my joy and instead of that, what am I doing?... - Yes, what is he doing? - I guess he's complaining!
Did you know: the only image of Michel Rolle available on the internet is, in fact, a low resolution picture of Leibnitz.
(Rolle is known by every French math student because the standard construction of analysis here goes through the theorem named after him, is it one of those cases where we're the only ones doing it this way or is the guy actually famous?)