International Conference on Functional Programming 2017

Effect-Driven QuickChecking of Compilers


Listen Later

Jan Midtgaard, gives the fourth presentation in the fourth panel, Effects, in the ICFP 2017 conference. Co-written by Mathias Nygaard Justesen, Patrick Kasting, Flemming Nielson, Hanne Riis Nielson, DTU, Denmark. How does one test a language implementation with QuickCheck (aka. property-based testing)? One approach is to generate programs following the grammar of the language. But in a statically-typed language such as OCaml too many of these candidate programs will be rejected as ill-typed by the type checker. As a refinement Pałka et al. propose to generate programs in a goal-directed, bottom-up reading up of the typing relation. We have written such a generator. However many of the generated programs has output that depend on the evaluation order, which is commonly under-specified in languages such as OCaml, Scheme, C, C++, etc. In this paper we develop a type and effect system for conservatively detecting evaluation-order dependence and propose its goal-directed reading as a generator of programs that are independent of evaluation order. We illustrate the approach by generating programs to test OCaml's two compiler backends against each other and report on a number of bugs we have found doing so.
...more
View all episodesView all episodes
Download on the App Store

International Conference on Functional Programming 2017By Oxford University


More shows like International Conference on Functional Programming 2017

View all
Philosophy for Beginners by Oxford University

Philosophy for Beginners

330 Listeners

Approaching Shakespeare by Oxford University

Approaching Shakespeare

334 Listeners

General Philosophy by Oxford University

General Philosophy

71 Listeners

Aesthetics and Philosophy of Art lectures by Oxford University

Aesthetics and Philosophy of Art lectures

77 Listeners

Theoretical Physics - From Outer Space to Plasma by Oxford University

Theoretical Physics - From Outer Space to Plasma

57 Listeners

Critical Reasoning: A Romp Through the Foothills of Logic by Oxford University

Critical Reasoning: A Romp Through the Foothills of Logic

39 Listeners

The Secrets of Mathematics by Oxford University

The Secrets of Mathematics

41 Listeners

Critical Reasoning for Beginners by Oxford University

Critical Reasoning for Beginners

32 Listeners

Literature and Form by Oxford University

Literature and Form

18 Listeners

CortexCast - A Neuroscience Podcast by Oxford University

CortexCast - A Neuroscience Podcast

4 Listeners