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.
Teaching
- 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
Publications
- 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
- [PDF]
- Automatische statische Kosten-Analyse für parallele Programme
- M.Sc Seminar, Ludwig-Maximilians-Universität München, 2017
- [PDF]
- Formalizing Types and Programming Languages in Isabelle/HOL
- B.Eng. Thesis, École de technologie supérieure, 2014
- [PDF]
- Defining (Co)datatypes in Isabelle/HOL
- Jasmin Christian Blanchette, M. D., Lorenz Panny, Andrei Popescu, and Dmitriy Traytel, Isabelle 2014 Release
- [PDF]
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
- [WEB]
- Lean Together 2019
- 7 Jan. 2019–11 Jan. 2019 | Amsterdam, The Netherlands
- [WEB]
- DSSS 2018: DeepSpec Summer School
- 16 Jul. 2018–27 Jul. 2018 | Princeton, New Jersey, United States
- [WEB]
- WAIT 2018: Fourth International Workshop on Automated (Co)inductive Theorem Proving
- 28 Jun. 2018–29 Jun. 2018 | Amsterdam, The Netherlands
- [WEB]
- Matryoshka 2018 : First European Workshop on Higher-Order Automated Reasoning
- 25 Jun. 2018–27 Jun. 2018 | Amsterdam, The Netherlands
- [WEB]
- TutorPlus: Basis-Zertifikat
- Apr. 2017–Jun. 2017 | LMU Munich, Germany
- [PDF]
- OPLSS 2015: Oregon Programming Language Summer School
- 15 Jun. 2015–27 Jun. 2015 | Eugene, Oregon, United States
- [WEB]
- VTSA 2014: Summer School on Verification Technology, Systems & Applications
- 27 Oct. 2014–31 Oct. 2014 | Luxembourg, Luxembourg
- [WEB]
Work Experience
- Universität der Bundeswehr München: Research Institute Cyber Defence (CODE)
-
Feb. 2018–-Aug. 2021 | Munich, Bavaria, Germany
Research Associate
- 3D EXCITE
-
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
- Ubisoft
-
Jan. 2013–Apr. 2013 | Montréal, Québec, Canada
Software Developer Intern
- Genetec
-
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
Languages
- French (native speaker)
- English (fluent)
- German (C1.2) (TestDaF 5,5,4,5)
- Latin (kleines Latinum)
Personal notes