[TYPES] Systematically testing type systems

Klaus Ostermann ostermann at informatik.tu-darmstadt.de
Tue Jul 4 06:13:35 EDT 2006

Hi all,

I hope this is not a stupid question, but I wonder whether it is feasible to 
test the soundness of a type checker by enumerating all programs in the 
language, reducing each program one step (assuming we have a small-step 
interpreter and a language where the full execution state is in the program 
itself) and checking whether subject reduction holds. If the enumeration of all 
programs would be smart enough (i.e., produce only syntactically correct 
programs; no two programs in the enumeration are alpha-equivalent) I could 
imagine that it would be feasible to test a type checker for all programs less 
than X bytes in size, where X is a reasonable number (e.g., 1KB) - at least for 
minimalistic languages as they are common in type research.

Has this ever been tried, or is it obvious that it would not work in practice?

Klaus Ostermann

More information about the Types-list mailing list