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
Past courses
Introduction à Python (IP1) - Université Paris Cité (L1)
Concepts Informatiques (CI2) - Université Paris Cité (L1)
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.
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.
publications
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.