Martin Desharnais

I am a PhD student in computer science at the Max-Planck-Institut für Informatik (Germany). Before that, I concluded a M.Sc. at the Ludwig-Maximilians-Universität München (Germany) and a B.Eng. in Software Engineering at the École de technologie supérieure (Canada).

My main fields of interest are programming languages, type systems, functional programming, formal verification, and static analysis.


Maschinennahe Programmierung Übung (Winter 2021)
B.Sc. course at Universität der Bundeswehr München, Germany
Main lecturer: Prof. Stefan Brunthaler
Language: German
Weekly exercices
Language-based Security (Summer 2019)
M.Sc. course at Universität der Bundeswehr München, Germany
Main lecturer: Prof. Stefan Brunthaler
Language: English
2019-05-14: Control-Flow Integrity
2019-05-21: Software Diversity, part 1
2019-06-04: Software Diversity vs BROP, COOP, JIT-Spraying
2019-06-18: Side Channels, Spectre & Meltdown


Reliable Reconstruction of Fine-grained Proofs in a Proof Assistant
Hans-Jörg Schurr, Mathias Fleury, Martin Desharnais
Conference on Automated Deduction (CADE) 2021
[Open Access]
Towards Efficient and Verified Virtual Machines for Dynamic Languages
Martin Desharnais, Stefan Brunthaler
Certified Programs and Proofs (CPP) 2021
[Open Access] [PDF (preprint)] [PDF (slides)]
A Generic Framework for Verified Compilers Using Isabelle/HOL's Locales
Martin Desharnais, Stefan Brunthaler
Isabelle Workshop 2020
[PDF (draft)] [slides]
A Generic Framework for Verified Compilers Using Isabelle/HOL's Locales
Martin Desharnais, Stefan Brunthaler
Journées Francophones des Langages Applicatifs (JFLA) 2020
[PDF (draft)] [slides] [Proceeding]
Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic
J Biendarra, J C Blanchette, A Bouzy, M Desharnais, M Fleury, J Hölzl, O Kunčar, A Lochbihler, F Meier, L Panny, A Popescu, C Sternagel, R Thiemann, and D Traytel, 11th International Symposium on Frontiers of Combining Systems, 2017
Automatische statische Kosten-Analyse für parallele Programme
M.Sc Seminar, Ludwig-Maximilians-Universität München, 2017
Formalizing Types and Programming Languages in Isabelle/HOL
B.Eng. Thesis, École de technologie supérieure, 2014
Defining (Co)datatypes in Isabelle/HOL
Jasmin Christian Blanchette, M. D., Lorenz Panny, Andrei Popescu, and Dmitriy Traytel, Isabelle 2014 Release

Academic Background

Max-Planck-Institut für Informatik
Sep. 2021– | Saarbrücken, Saarland, Germany
Computer Science
Cosupervisor: Dr. Jasmin Blanchette
Cosupervisor: Dr. Sophie Tourret
Cosupervisor: Prof. Dr. Christoph Weidenbach
Universität der Bundeswehr München
Feb. 2019–Aug. 2021 | Munich, Bavaria, Germany
Computer Science
Ludwig-Maximilians-Universität München
Apr. 2016–Nov. 2018 | Munich, Bavaria, Germany
M.Sc. Computer Science
Average grade (German system): 1.20 (120 ECTS)
École de technologie supérieure
Sep. 2011–Aug. 2015 | Montréal, Québec, Canada
B.Eng. Software Engineering
Average grade (Quebec system): 3,91/4,30 (264 ECTS)
Cégep de Trois-Rivières
Aug. 2008–Mai 2011 | Trois-Rivières, Québec, Canada
DCS Computer Science Technology

Extra-Academic Background

PC 2019: Autumn school "Proof and Computation"
70 Sep. 2019–26 Sep. 2019 | Herrsching, Germany
Lean Together 2019
7 Jan. 2019–11 Jan. 2019 | Amsterdam, The Netherlands
DSSS 2018: DeepSpec Summer School
16 Jul. 2018–27 Jul. 2018 | Princeton, New Jersey, United States
WAIT 2018: Fourth International Workshop on Automated (Co)inductive Theorem Proving
28 Jun. 2018–29 Jun. 2018 | Amsterdam, The Netherlands
Matryoshka 2018 : First European Workshop on Higher-Order Automated Reasoning
25 Jun. 2018–27 Jun. 2018 | Amsterdam, The Netherlands
TutorPlus: Basis-Zertifikat
Apr. 2017–Jun. 2017 | LMU Munich, Germany
OPLSS 2015: Oregon Programming Language Summer School
15 Jun. 2015–27 Jun. 2015 | Eugene, Oregon, United States
VTSA 2014: Summer School on Verification Technology, Systems & Applications
27 Oct. 2014–31 Oct. 2014 | Luxembourg, Luxembourg

Work Experience

Universität der Bundeswehr München: Research Institute Cyber Defence (CODE)
Feb. 2018–-Aug. 2021 | Munich, Bavaria, Germany
Research Associate
Mai 2017–Nov. 2018 | Munich, Bavaria, Germany
Compiler Developer
Ludwig-Maximilians-Universität München: Chair of computer science (Prof. Martin Hofmann)
Apr. 2018–Aug. 2018 | Munich, Bavaria, Germany
Teaching Assistant
Ludwig-Maximilians-Universität München: Chair for programming and modelling languages (Prof. François Bry)
Apr. 2017–Aug. 2017 | Munich, Bavaria, Germany
Teaching Assistant
Technische Universität München: Chair for logic and verification (Prof. Tobias Nipkow)
May 2014–Dec. 2014 | Munich, Bavaria, Germany
Research Assistant Intern
AGA Financial Group
2013– | Westmount, Québec, Canada
Software Developer
Jan. 2013–Apr. 2013 | Montréal, Québec, Canada
Software Developer Intern
Jan. 2012–Apr. 2012 | Montréal, Québec, Canada
Software Developer Intern
ICO Technologies
Jan. 2011–Aug. 2011 | Shawinigan, Québec, Canada
Software Developer
AGA Financial Group
May 2010 – Aug. 2010 | Westmount, Québec, Canada
Computer Technician Intern
IGA Grenier Fortin
2008–2011 | Trois-Rivières, Québec, Canada
Grocery Clerk
Jardins Dugrés
2005–2007 | Trois-Rivières, Québec, Canada
Agricultural Labourer


Personal notes