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.

Publications

An Isabelle/HOL Formalization of the SCL(FOL) Calculus: Martin Bromberger, Martin Desharnais, and Christoph Weidenbach
CADE 29: 29^th International Conference on Automated Deduction (2023)
[Open Access]
Seventeen Provers Under the Hammer: Martin Desharnais, Petar Vukmirović, Jasmin Blanchette, and Makarius Wenzel
ITP 2022: 13^th International Conference on Interactive Theorem Proving
[Open Access]
Reliable Reconstruction of Fine-grained Proofs in a Proof Assistant: Hans-Jörg Schurr, Mathias Fleury, Martin Desharnais
CADE 28: 28^th International Conference on Automated Deduction (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
[Open Access] [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
11^th 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, Martin Desharnais, Lorenz Panny, Andrei Popescu, and Dmitriy Traytel
Isabelle 2014 Release
[PDF]

Formalizations

A Formalization of the SCL(FOL) Calculus: Simple Clause Learning for First-Order Logic: Isabelle/HOL
Archive of Formal Proofs, 2023
AFP/Simple_Clause_Learning
Inline Caching and Unboxing Optimization for Interpreters: Isabelle/HOL
Archive of Formal Proofs, 2020
AFP/Interpreter_Optimizations
A Generic Framework for Verified Compilers: Isabelle/HOL
Archive of Formal Proofs, 2020
AFP/VeriComp

Academic Background

Max-Planck-Institut für Informatik: Sep. 2021– | Saarbrücken, Saarland, Germany
PhD Student in Computer Science
Cosupervisor: Prof. Dr. Christoph Weidenbach
Cosupervisor: Prof. Dr. Jasmin Blanchette
Cosupervisor: Dr. Sophie Tourret \
Ludwig-Maximilians-Universität München: Apr. 2016–Nov. 2018 | Munich, Bavaria, Germany
M.Sc. Computer Science
Average grade (German system, lower is better): 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, higher is better): 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”: 20 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

Max-Planck-Institut für Informatik: Sep. 2021– | Saarbrücken, Saarland, Germany
Research Associate
AGA Financial Group: 2013– | Westmount, Québec, Canada Software Developer
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
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

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

Languages

French (native speaker)
English (fluent)
German (C1.2) (TestDaF 5,5,4,5)
Latin (kleines Latinum)