ESOP 2015
Tue 14 - Thu 16 April 2015 London, United Kingdom
Wed 15 Apr 2015 14:00 - 14:30 at Skeel - Session 5 Chair(s): Jan Vitek

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.

Wed 15 Apr

Displayed time zone: Azores change

14:00 - 16:00
Session 5ESOP at Skeel
Chair(s): Jan Vitek Northeastern University
14:00
30m
Talk
Making Random Judgments: Automatically Generating Well-Typed Terms from the Definition of a Type-System
ESOP
Burke Fetscher Northwestern University, Koen Claessen Chalmers University of Technology, Michał Pałka Chalmers University of Technology, John Hughes Chalmers University of Technology, Robert Bruce Findler Northwestern University
14:30
30m
Talk
Refinement Types for Incremental Computational Complexity
ESOP
Ezgi Çiçek MPI-SWS, Deepak Garg MPI-SWS, Umut A. Acar Carnegie Mellon University
15:00
30m
Talk
Monotonic References for Efficient Gradual Typing
ESOP
Jeremy G. Siek Indiana University, Michael M. Vitousek Indiana University, Matteo Cimini Indiana University, Sam Tobin-Hochstadt Indiana University, Ronald Garcia University of British Columbia
15:30
30m
Talk
Inter-procedural Two-Variable Herbrand Equalities
ESOP
Stefan Schulze Frielinghaus Technische Universität München, Michael Petter Technische Universität München, Helmut Seidl Technische Universität München