Making Random Judgments: Automatically Generating Well-Typed Terms from the Definition of a Type-System

This paper presents a generic method for randomly generating well-typed expressions. It starts from a specification of a typing judgment in PLT Redex and uses a specialized solver that employs randomness to find many different valid derivations of the judgment form. Our motivation for building these random terms is to more effectively falsify conjectures as part of the tool-support for semantics models specified in Redex. Accordingly, we evaluate the generator against the other available methods for Redex, as well as the best available custom well-typed term generator. Our results show that our new generator is much more effective than generation techniques that do not explicitly take types into account and is competitive with generation techniques that do, even though they are specialized to particular type-systems and ours is not.

Lindström Claessen, Koen,1975Chalmers tekniska högskola,Chalmers University of Technology(Swepub:cth)koen (författare)
Palka, Michal,1983Chalmers tekniska högskola,Chalmers University of Technology(Swepub:cth)palka (författare)
Hughes, John,1958Chalmers tekniska högskola,Chalmers University of Technology(Swepub:cth)rjmh (författare)
Findler, R. B.Northwestern University (författare)
Northwestern UniversityChalmers tekniska högskola (creator_code:org_t)

Ingår i:Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)Berlin, Heidelberg : Springer Berlin Heidelberg9032, s. 383-4051611-33490302-9743

Av författaren/redakt...: Fetscher, B.; Lindström Claess ...; Palka, Michal, 1 ...; Hughes, John, 19 ...; Findler, R. B.

Om ämnet

NATURVETENSKAP: NATURVETENSKAP; och Data och informa ...; och Systemvetenskap ...

Kungliga biblioteket hanterar dina personuppgifter i enlighet med EU:s dataskyddsförordning (2018), GDPR. Läs mer om hur det funkar här.
Så här hanterar KB dina uppgifter vid användning av denna tjänst.