Making random judgments: Automatically generating well-typed terms from the definition of a type-system

Burke Fetscher, Koen Claessen, Michał Pałka, John Hughes, Robert Findler

Research output: Chapter in Book/Report/Conference proceedingConference contribution

19 Scopus citations

Abstract

This paper presents a generic method for randomly generating welltyped 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.

Original languageEnglish (US)
Title of host publicationProgramming Languages and Systems - 24th European Symposiumon Programming, ESOP 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, Proceedings
EditorsJan Vitek
PublisherSpringer Verlag
Pages383-405
Number of pages23
ISBN (Electronic)9783662466681
DOIs
StatePublished - 2015
Event24th European Symposium on Programming, ESOP 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015 - London, United Kingdom
Duration: Apr 11 2015Apr 18 2015

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9032
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other24th European Symposium on Programming, ESOP 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015
CountryUnited Kingdom
CityLondon
Period4/11/154/18/15

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Making random judgments: Automatically generating well-typed terms from the definition of a type-system'. Together they form a unique fingerprint.

Cite this