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+ ]

teaching

Current courses

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

HTTP basics HTML CSS PHP MySQL JavaScript Project (website)

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

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

Propositional logics Logical circuits Positional numeration Two's complement IEEE-754 Coding theory Compression Error control Cryptography

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

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

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

Reminders on Java Classes/Objects Function overloading Inheritance and dispatch Interfaces Common OO patterns

projects

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.

Type system Prototype Polymorphism Intesection types Occurence typing OCaml

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

GBA Pokemon Glitch ACE OCaml

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

GBA ROM hacking Level editor Kururin C#

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

PC Bot VVVVVV Python Julia

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

GBA TAS Tool Assisted Speedrun Kururin Bot C#

publications

Giuseppe Castagna, Mickaël Laurent & Kim Nguyen
We present a type system that combines, in a controlled way, first-order polymorphism with intersectiontypes, union types, and subtyping, and prove its safety. This makes the system a prime candidate to type dynamic languages.

Set-theoretic types Semantic subtyping Intersection types Union types Occurrence typing Type narrowing Dynamic language Type inference Polymorphism

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.

Set-theoretic types Semantic subtyping Intersection types Union types Occurrence typing Union elimination Typecases Type inference

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.

Set-theoretic types Semantic subtyping Occurrence typing Gradual typing Typecases

Wait! There's more...

experience

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

education

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)