Mickaël Laurent

Paris, France · mlaurent@irif.fr

Hi! 👋 I'm a PhD student in computer science at IRIF (Paris, France) supervised by Giuseppe Castagna and Kim Nguyen, in the pole PPS.

  • 🤓 I’m interested in programming languages, especially (strongly) typed ones :)
  • ⚙️ Please try the web version of my type system prototype
  • 🕹️ On my free time, I like playing co-op video games and watching speedruns and e-sport competitions
  • 🛠️ I also practice glitch hunting, Tool Assisted Speedrun, ROM hacking and other technical stuff
  • 📫 How to reach me: mlaurent@irif.fr. Or in person: office 3033 of the Sophie Germain building
  • 🔗 GitHub - ORCID - YouTube

You can also read my PDF resume.

And if you are gourmand, here are some generous types:

map: (('b -> 'a) -> [ 'b* ] -> [ 'a* ]) & (Any -> [  ] -> [  ])
filter: ('a -> Any) & ('b -> Any \ `true) -> [ ('a | 'b)* ] -> [ ('a \ 'b)* ]
flatten: X1 -> [ 'a* ] where X1 = [ X1* ] | 'a \ [ Any+ ]


Current courses

Principe de Fonctionnement des Machines Binaires (PF1) - Université Paris Cité (L1)

Internet et Outils (IO2) - Université Paris Cité (L1)

Programmation Orientée Objet (POO3) - Université Paris Cité (L2)

Programmation réseau (PR6) - Université Paris Cité (L3)

Past courses

Introduction à Python (IP1) - Université Paris Cité (L1)

Expressions/instructions Basic control flow Functions Character encoding Lists Matrices and imbricated loops

Concepts Informatiques (CI2) - Université Paris Cité (L1)

Recursive data structures Memory layout (stack, heap) Compilation Imperative vs functional Tail recursion


A collection of professional, academic and personal projects.

A prototype in OCaml for my research about typing dynamic languages with parametric polymorphism and intersection types.

A generator of codes for achieving Arbitrary Code Execution in some Pokemon games.

A level editor for the GBA games Kuru Kuru Kururin and Kururin Paradise.

Two different bots (DQN vs search-based) that play the super-gravitron of the game VVVVVV.

A Tool Assisted Speedrun (TAS) full of glitches, for the GBA game Kuru Kuru Kururin.


Giuseppe Castagna, Mickaël Laurent, Kim Nguyen & Matthew Lutze
We extend classic union and intersection type systems with a type-case construction and show that the combination of the union elimination rule of the former and the typing rules for type-cases of our extension encompasses occurrence typing.

Giuseppe Castagna, Victor Lanvin, Mickaël Laurent & Kim Nguyen
We revisit occurrence typing, a technique to refine the type of variables occurring in type-cases and, thus, capture some programming patterns used in untyped languages.

Daniel Larraz, Mickaël Laurent & Cesare Tinelli
We introduce two new major features of the open-source model checker Kind 2 which provide traceability information between specification and design elements such as assumptions, guarantees, or other behavioral constraints in synchronous reactive system models.


Oregon Programming Languages Summer School (Eugene, USA)

Participation to a summer school in Oregon. Lectures were given by experts in the programming language area.

University of Iowa - Electrical and Computer Engineering (Iowa City, USA)

Research internship. Development of traceability analysis tools in the SMT-based model-checker Kind2. Supervisor: Cesare Tinelli

Laboratoire Methodes Formelles - VALS Team (Saclay, France)

Research internship. Formalisation of a type system featuring occurence typing and set-theoretic types. Supervisor: Kim Nguyen

Carnegie Mellon University - Cylab (Pittsburgh, USA)

Research internship. Conception of a method for interactive loop invariant synthesis, in a decidable fragment of first-order logic. Supervisor: Bryan Parno

Carnegie Mellon University - Computer Science Department (Pittsburgh, USA)

Research internship. Counterfactual causal analysis in a rule-based language modelling cellular signaling. Supervisor: Jean Yang


PhD of Computer Science

Type Systems, Programming Languages, Logics, Verification
Title: Type inference for dynamic languages, using set-theoretic types and parametric polymorphism

Master of Computer Science

Functional programming, Automata theory, Verification, Algorithmics
Title: Algorithms and Foundations of Programming (MPRI)

Preparatory classes for the Grandes Ecoles

Mainly Mathematics and Physics, with some Computer Science and Literature
Title: MPSI (1st year), MP* (2nd year)