Set-theoretic types support expressive record types through unions, intersections, and negations, but they lack the row polymorphism needed to type operations that propagate unknown fields across records. Prior work addresses this by allowing Boolean combinations of rows in type substitutions, which complicates the formalism and prevents the tallying algorithm from being complete. We propose an alternative: instead of enriching substitutions, we allow Boolean combinations of row variables directly within record type constructors, where the tail of a record has the same shape as any field. This design keeps substitutions simple—a row variable maps to a single row—and yields a natural extension of the subtyping and tallying algorithms. Tallying is complete for all solutions whose rows are constant over labels not mentioned in the constraints. We implement our approach in the set-theoretic type library SSTT and the type checker MLsem, providing the first implementation of a type system that combines semantic subtyping with row polymorphism. We demonstrate the expressiveness of the system by encoding several data structures from the R programming language: heterogeneous lists, variadic function arguments, and class-based dispatch.

Set-theoretic types provide a rich type algebra that supports unrestricted unions, intersections, and negations, together with a decidable type constraint-solving algorithm known as tallying. These types are particularly well suited for typing dynamic languages, where functions often exhibit both generic and overloaded behavior. However, the complexity of their implementation has hindered their widespread adoption. In this paper, we introduce a modular representation for set-theoretic types and revisit the algorithms for subtyping and tallying. We compare our approach with the historical CDuce implementation and evaluate the performance impact of some optimizations and design choices.

Dynamic programming languages pose significant challenges for optimizing compilers due to features such as dynamic typing, late binding, reflection, copy-on-write, and delayed evaluation. To generate efficient code, compilers must speculate on which dynamic features will be exercised and produce specialized code based on these assumptions. This paper presents the design of a statically typed, high-level intermediate representation that makes dynamic behaviors explicit and amenable to static analysis. Our IR combines gradual typing with ownership tracking, and explicitly represents promises, multiple function versions, and contextual dispatch. Together, these features directly support optimizations such as specialization, inlining, scope elision, and copy elimination. We formalize a core calculus, called FIR, that captures the essential features required for these optimizations. We provide an operational semantics, a type system, and flow and reflection analyses, and we prove the soundness of the type system.

This paper serves as a celebration of the twenty-fifth anniversary of Kuru Kuru Kururin. Although this video game is presented as a collection of two-dimensional puzzles based on rotation, it naturally invites players to complete its levels as quickly as possible. This has led to a surprisingly rich and challenging playing field to finding foremost temporal walks. In this work, we tackle this problem both in theory and in practice.

In this paper, we formalize a type system based on set-theoretic types for dynamic languages that support both functional and imperative programming paradigms. We adapt prior work in the typing of overloaded and generic functions to support an impure 𝜆-calculus, focusing on imperative features commonly found in dynamic languages such as JavaScript, Python, and Julia. We introduce a general notion of parametric opaque data types using set-theoretic types, enabling precise modeling of mutable data structures while promoting modularity, clarity, and readability. Finally, we compare our approach to existing work and evaluate our prototype implementation on a range of examples.

Compilers for dynamic languages often rely on intermediate representations with explicit type annotations to facilitate writing program transformations. This paper documents the design of a new typed intermediate representation for a just-in-time compiler for the R programming language called FIŘ. Type annotations, in FIŘ, capture properties such as sharing, the potential for effects, and compiler speculations. In this extended abstract, we focus on the sharing properties that may be used to optimize away some copies of values.

We present a type system that combines, in a controlled way, first-order polymorphism with intersection types, union types, and subtyping, and prove its safety. We then define a type reconstruction algorithm that issound and terminating. This yields a system in which unannotated functions are given polymorphic types(thanks to Hindley-Milner) that can express the overloaded behavior of the functions they type (thanks tothe intersection introduction rule) and that are deduced by applying advanced techniques of type narrowing(thanks to the union elimination rule). This makes the system a prime candidate to type dynamic languages.

This paper describes several new features of the open-source model checker Kind 2. Its input language and model checking engines have been extended to allow users to model and reason about systems with machine integers. In addition, Kind 2 can now provide traceability information between specification and design elements, which can be used for several purposes, including assessing the quality of a system specification, tracking the safety impact of model changes, and analyzing the tolerance and resilience of a system against faults or cyber-attacks. Finally, Kind 2 is also able to check whether a component contract is realizable or not, and provide a deadlocking computation and a set of conflicting guarantees when the contract is unrealizable.

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. To apply this system in practice, we define a canonical form for the expressions of our extension, called MSC-form. We show that an expression of the extension is typable if and only if its MSC-form is, and reduce the problem of typing the latter to the one of reconstructing annotations for that term. We provide a sound algorithm that performs this reconstruction and a proof-of-concept implementation.

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. Although occurrence typing was tied from its inception to set-theoretic types—union types, in particular—it never fully exploited the capabilities of these types. Here we show how, by using set-theoretic types, it is possible to develop a general typing framework that encompasses and generalizes several aspects of current occurrence typing proposals and that can be applied to tackle other problems such as the reconstruction of intersection types for unannotated or partially annotated functions and the optimization of the compilation of gradually typed languages.

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. This new version of Kind 2 can identify minimal sets of design elements, known as Minimal Inductive Validity Cores, which are sufficient to prove a given set of safety properties, and also determine the set of MUST elements, design elements that are necessary to prove the given properties. In addition, Kind 2 is able to find minimal sets of design constraints, known as Minimal Cut Sets, whose violation leads the system to an unsafe state. We illustrate with an example how to use the computed information for tracking the safety impact of model changes, and for analyzing the tolerance and resilience of a system against faults.

A type checker prototype for functional and imperative dynamic languages, implemented in OCaml, and featuring:

• Set-theoretic types (with intersection, union, negation and recursive types)
• Ad-hoc polymorphism to capture overloaded behaviors
• Parametric polymorphism (and row-polymorphism) to capture genericity
• Precise typing of type-cases and pattern matching (occurrence typing)
• Type inference (with optional user type annotations)
• Imperative programming (references, mutable arrays, etc.)
• Opaque data types
• Gradual typing

SSTT is an OCaml library for manipulating set-theoretic types. Currently, it supports the following type constructors:

• Enums
• Tags
• Integer intervals
• Arrows
• Tuples of any arity
• Records
• Type variables and row variables
• Many extensions (opaque parametric data types, lists, etc.)

The following operations are implemented:

• Semantic subtyping
• DNF extraction and simplification
• Projections, application, record merging
• Substitution
• Tallying (= unification but with subtyping constraints)
• Pretty printing (or more generally, extraction of an algebraic representation)

I think the game I played the most when I was a kid was Pokemon Ruby, on GBA. With my brother, we completed the regional Pokedex, with 200/200 Pokemon catched. Unfortunately, there still were two Mythical Pokemons that we were unable to catch, and for a good reason: those were accessible only for those attending some physical events, occuring only in some places and sometimes only in Japan. This was the early time of forums, and lot of rumors started to flourish: you can unlock Deoxys by beating the Battle Tower, by waiting for the white stone of the spatial center to be stolen, etc... But rumors, that's all they were.

In 2021, I got interested into the glitching scene, that is, how to exploit bugs and flaws in games in order to do things that the developers did not plan. That's where I discovered that this wasn't a lie: it is indeed possible to catch Deoxys without attending physical events nor using any cheating device! There are several methods to achieve it, but the most reliable and powerful way is via Arbitrary Code Execution (ACE). It is the Holy-Grail of glitchers: exploiting the game until we are able to make it execute any code we want! If I find some time, I'll write something about it, because the process to get there is very interestig in a technical point of view. What's ironic is that it is only possible to achieve that thanks to... the protections added to the game by the developpers in order to make cheating more difficult (in particular, a very basic kind of ASLR and some checksum verifications) 🤦‍♂️

But achieving ACE is not an easy task: you have to write some code in the memory, and then make the game execute it. Both aspects are very interesting, but the tool I made focuses on the first one: how to write machine code (ARM7TDMI) in a specific location in memory. For that, we use a mechanic of the game that allows us to rename boxes of the in-game PC (where we store our pokemons): it consists of 14 names of 8 characters each. Those 14 names are stored consecutively in memory, one byte for each character, but are separated by a 0xFF byte (the EOF character). Thus, it takes in total (8+1)*14=126 bytes.

The main issue is that only about 1/3 of the 256 possible values for each byte can be written, due to the character encoding used by the game. So, we have to write machine code (using one of the ARM or Thumb instruction sets), but by being unable to write 2/3 of the possible byte values... That sounds like an impossible constraint! Fortunately, while it seems very complicated to write Thumb code with this constraint, it is possible, to write some very useful ARM opcodes: some arithmetic ones (ADC,SBC), and some memory-related ones (MOV,STR(H),LDR(H)). Of course, only a small subset of registers and immediate constants are accessible due to the constraint on the charset. But it is enough to write abritrary code: by doing the right arithmetic operations using MOV, ADC and SBC, we can compute any opcode we want in a register, and then write it a little ahead of the current instruction (PC register), using a command STR, for it to be executed.

Another constraint is the presence of a 0xFF byte (EOF), which cannot be modified, at the end of each box name. It forces us to insert some dummy machine instructions that do nothing but contain this EOF byte. After that, we just have to convert the machine code we obtain into characters using the character encoding, and we are done.

This whole process is what the tool I made automates. It parses some ARM assembly code written by the user (with some preprocessor extensions), finds a way to write immediate values using writable arithmetic operations, assembles them and encodes the result, for finally showing the box names one has to enter in the game! Using this code generator, it is also possible to setup a much more powerful ACE environment, for instance by bootstrapping a code that allows you to get rid of the limitations cited above. You can take a look at this video that shows a full exploitation of ACE in order to inject a new Pokemon species in the game!

In 2020, one year after my TAS of Kuru Kuru Kururin, I decided to investigate the code of this GBA game furthermore and make an editor that allows to edit the maps of the game. Armed with an emulator and a debugger, I tried to document where and how maps are stored, to extract the tiles and palettes for each level, etc. Finally, I managed to make a level editor!

My friend mohoc7 used it to create an insane(ly difficult) ROM-hack that you can download here 😁 (and it works on a real GBA: I've tested it)! I have also adapted the level editor to support the sequel of the game, Kururin Paradise, with the help of Dimedime!

The source code of the PC game VVVVVV got officialy released in 2020. It was announced by my friend mohoc7, during his speedrun of this game at the AGDQ 2020. This motivated me to dig in the source code and see what I could do... and I finally decided to make a bot for the Super-Gravitron (a mode of the game where we have to avoid projectiles)!

I first made a Python bot using an implementation of a DQN in order to learn to play this game, as it was done by Google for some Atari games (link). For that, I built a customized version the game where inputs are taken from the console, and where game states are logged in the console too (Github).

Then, deceived by the result (though it was performing way better than the average human, it did not break the ~10min record of my friend!), I decided to make another bot, this time without using machine learning. I replicated the physics of the game in Julia (which offers better performance than Python), and made a bot that searches a trajectory based on this simulation of the game. This time it broke the record... 💪

In 2019, I made a Tool Assisted Speedrun (TAS) with a classmate and dear friend, mohoc7. While mohoc was the expert of the game and director of the TAS, I was the technical team. If you watched the video of the TAS, you might be thinking "well, this game is totally broken, look how it is easy to clip in the walls!". But if you try it yourself, you might be surprised how difficult it is! Actually, clipping in a wall without the help of a moving object is not humanly feasible (update: it actually is). In a TAS, we can tell the emulator to press on each frame the buttons we want: the challenge is to find a sequence of button presses that finishes the game as quickly as possible. Even with an emulator that can press buttons for us, clipping through a wall is quite complicated: for instance, another TASer, Ryuto, made a TAS years before ours without even noticing such a mechanics was possible.

So, how to achieve wall-clipping? You can find an explanation of how it works on tasvideo.org, but the conclusion is that there is no systematic way to achieve it! It relies on a very precise combination of position, velocity and collision mask, and the only way we found in order to be able to achieve it in different situations is to make a bot that tries a lot of paths. At first, I tried to make a script that communicates with the game in order to test different paths, but we abandonned this approach: it was too slow. Instead, I replicated the exact physics of the game, from the logic of collisions to the computation of trigonometric functions with the right precision!

In order to search paths, I basically used an A* algorithm with a custom cost map computed with a flooding algorithm. Some optimisations and approximations were necessary in order to reduce the search space, but in the end, it worked! However, due to the approximations and heuristics used, there is no guarantee of optimality in the results produced. Stil, this was a great challenge, both algorithmically and technically, and I really like the result 😁!