Write a Blog >>
ICFP 2018
Sun 23 - Sat 29 September 2018 St. Louis, Missouri, United States
Fri 28 Sep 2018 09:00 - 10:00 at Burlington Route - Invited Talk 1

Programmers are rapidly adopting expressive, dynamically typed, higher-order functional programming languages for their everyday development tasks. Over time, these programs are often fortified with static type checking by migrating programs using gradual types, a technique now widely used by the largest industrial software development companies. Unfortunately, there are limits both to what properties gradual types can validate and the help they can provide programs as they engage in the migration process. In parallel, researchers have developed sophisticated next generation programming languages with integrated verification features. These languages are able to validate much stronger claims about the correctness of software, but their industrial adoption has lagged far behind gradual typing. Consequently, verification is not being integrated in the everyday lives of programmers and the quality and reliability of software suffers because of it. This represents a tremendous missed opportunity considering the rapid advancement of automated verification techniques.

In this talk, I’ll talk about our recent efforts to close the expressivity gap between the everyday languages of programmers and these verification-integrated languages, enabling pathways to verified programming at every point along the spectrum scripting languages to theorem proving languages.

Fri 28 Sep

Displayed time zone: Guadalajara, Mexico City, Monterrey change

09:00 - 10:00
Invited Talk 1Scheme at Burlington Route
09:00
60m
Talk
From Scripting to Proving: Gradual Verification with a Scheme
Scheme
David Van Horn University of Maryland, USA