ICFP/SPLASH 2025
Sun 12 - Sat 18 October 2025 Singapore
Sun 12 Oct 2025 16:00 - 16:30 at Seminar Room 2 - Session 3 Chair(s): Sosuke Moriguchi

“Fuzzing” is a popular testing approach where we throw random inputs at a program and check that it respects some expected properties on all inputs. Fuzzing a metaprogram such as a compiler requires producing random input programs. To exercise interesting behaviors of the compiler, we want our input programs to be well-formed in a strong sense, in particular to be well-typed. Generating random well-typed program is difficult when the type-system is powerful, there is a whole scientific literature on the topic, see for example [Testing an Optimising Compiler by Generating Random Lambda Terms, Pałka, 2012].

Most existing generators integrate a large part of the implementation of a type-checker, “inverted” to assist in top-down random term generation by efficiently discarding choices that result in ill-typed programs. Scaling this approach to a full language would result in implementing two sophisticated type-checkers, once in the compiler and once in the program generator. This is one type-checker too many!

We present preliminary work on reusing the constraint-based type inference approach [The Essence of ML-based type inference, Pottier and Rémy, 2004] to write a single type-checker that can be used for both purposes: to check types of user-provided programs, and to efficiently guide a random program generator. This only requires a fairly simple modification to constraint generators: parametrizing them over a search monad. We have succesfully implemented a generator of simply-typed terms in this style, and are in the process (almost done) of scaling it to Hindley-Milner type inference.

(Relevant previous work is [Making Random Judgments: Automatically Generating Well-Typed Terms from the Definition of a Type-System, Fetscher, Claessen, Pałka, Hughes, Findler]. They start from Redex, a Racket DSL to implement simple type systems, and derive a random program generator. The limitation of this approach is that Redex only works with fairly simple type system, in particular we do not expect it to scale to ML-style type inference with polymorphism, which is the part that hand-crafted generators also struggle on.)

Sun 12 Oct

Displayed time zone: Perth change

16:00 - 17:30
Session 3TyDe at Seminar Room 2
Chair(s): Sosuke Moriguchi Institute of Science Tokyo
16:00
30m
Talk
Constrained generation of well-typed programs (Extended Abstract) [Remote]
TyDe
Hugo Barreiro École Polytechnique, Gabriel Scherer Université Paris Cité - Inria - CNRS
16:30
30m
Talk
Type-Driven Prompt Programming: From Typed Interfaces to a Calculus of Constraints (Extended Abstract) [Remote]
TyDe
Abhijit Paul Samsung R&D Institute, Bangladesh
17:00
30m
Talk
A Formalization of Opaque Definitions for a Dependent Type Theory [Remote]
TyDe
Nils Anders Danielsson University of Gothenburg, Eve Geng Chalmers University of Technology, Gothenburg, Sweden