Martin Desharnais

I am a PhD student in computer science at the Universität der Bundeswehr München (Germany). Before that, I concluded a M.Sc. at the Ludwig-Maximilians- Univsersitä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.

Academic Background

Universität der Bundeswehr München
Feb. 2019– | Munich, Bavaria, Germany
Dr. rer. nat. Computer Science
Supervisor: Univ.-Prof. Dr. Stefan Brunthaler
Cosupervisor: Dr. Jasmin Blanchette
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

Teaching Experience

Language-based Security (Summer trimester 2019)
Universität der Bundeswehr München, Germany
INF Master (Modul 5507)
Dozent: 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

Work Experience

Universität der Bundeswehr München: Research Institute Cyber Defence (CODE)
Feb. 2018– | Munich, Bavaria, Germany
Research Associate
Mai 2017–Nov. 2018 | Munich, Bavaria, Germany
Compiler Developer
Ludwigs-Maximilians-Universität: Chair of computer science (Prof. Martin Hofmann)
Apr. 2018–Aug. 2018 | Munich, Bavaria, Germany
Teaching Assistant
Ludwigs-Maximilians-Universität: 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


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


Personal notes