Write a Blog >>
Sat 25 Jan 2020 16:50 - 17:20 at Orleans - Analysis, verification, blame Chair(s): Niki Vazou

This paper introduces λdB, a blame calculus with dependent types. It supports dependent functions, predicate refinement at all types, the dynamic type, and full blame tracking. It is inspired by and extends previous work on hybrid types and Sage, by Flanagan and others; manifest contracts, by Greenberg, Pierce, and Weyrich; and blame calculus by Wadler and Findler. While previous work only allows refinement over base types, λdB supports refinement over any type. We introduce novel techniques in order to prove blame safety for this language, including a careful analysis that reduces open judgments on terms to closed ones on values, and the idea of ‘subtyping with a witness’, which fix flaws in the previous work of Wadler and Findler. These technical contributions mean that we can achieve a completely inductive (finitistic) account of the metatheory of our language, and thereby avoid many of the subtle technical issues which have bedevilled earlier work in this area.

Sat 25 Jan

Displayed time zone: Saskatchewan, Central America change

15:35 - 17:45
Analysis, verification, blameWGT at Orleans
Chair(s): Niki Vazou IMDEA Software Institute
15:35
32m
Talk
Gradual Verification of Recursive Heap Data Structures
WGT
Jenna DiVincenzo (Wise) Carnegie Mellon University, Johannes Bader Facebook, Jonathan Aldrich Carnegie Mellon University, Éric Tanter University of Chile, Joshua Sunshine Carnegie Mellon University
Pre-print
16:07
33m
Talk
Gradual Program Analysis
WGT
Samuel Estep Liberty University, Jenna DiVincenzo (Wise) Carnegie Mellon University, Jonathan Aldrich Carnegie Mellon University, Éric Tanter University of Chile, Johannes Bader Facebook, Joshua Sunshine Carnegie Mellon University
Pre-print
16:40
10m
Break
Minibreak
WGT

16:50
30m
Talk
Blame tracking at higher fidelity
WGT
Jakub Zalewski University of Edinburgh, James McKinna University of Edinburgh, J. Garrett Morris University of Kansas, USA, Philip Wadler University of Edinburgh, UK
Pre-print
17:20
25m
Day closing
Discussion on gradual typing and WGT21
WGT