[TYPES] Systematically testing type systems
david.nospam.hopwood at blueyonder.co.uk
Wed Jul 5 12:31:56 EDT 2006
Klaus Ostermann wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 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?
It is obvious that it would not work in practice for programs up to 1 Kbyte.
It could only work for programs up to a few tokens in length.
David Hopwood <david.nospam.hopwood at blueyonder.co.uk>
More information about the Types-list