Thu 16 Jun 2016 16:30 - 17:00 at Grand Ballroom San Rafael - Types II Chair(s): Jean Yang

This paper presents a novel automated procedure for discovering expressive shape specifications for sophisticated functional data structures. Our approach extracts potential shape predicates based on the definition of constructors of arbitrary user-defined inductive data types, and combines these predicates within an expressive first-order specification language using a lightweight data-driven learning procedure. Notably, this technique requires no programmer annotations, and is equipped with a type-based decision procedure to verify the correctness of discovered specifications. Experimental results indicate that our implementation is both efficient and effective, capable of automatically synthesizing sophisticated shape specifications over a range of complex data types, going well beyond the scope of existing solutions.

Thu 16 Jun

Displayed time zone: Tijuana, Baja California change

15:30 - 17:00
Types IIResearch Papers at Grand Ballroom San Rafael
Chair(s): Jean Yang Carnegie Mellon University
15:30
30m
Talk
Just-in-Time Static Type Checking for Dynamic Languages
Research Papers
Brianna M. Ren University of Maryland, College Park, Jeffrey S. Foster University of Maryland, College Park
Media Attached
16:00
30m
Talk
Types from data: Making structured data first-class citizens in F#
Research Papers
Tomas Petricek University of Cambridge, UK, Don Syme Microsoft, Gustavo Guerra Microsoft Corporation, London
Pre-print Media Attached
16:30
30m
Talk
Automatically Learning Shape Specifications
Research Papers
He Zhu Purdue University, Gustavo Petri LIAFA, Université Paris Diderot, Suresh Jagannathan Purdue University
Media Attached