Colloquium Details
From Scripting to Proving: Gradual Verification for Expressive Programming Languages
Speaker: David Van Horn, University of Maryland
Location: 60 Fifth Avenue 150
Date: March 11, 2019, 2 p.m.
Host: Subhash Khot
Synopsis:
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 will give an overview of my group's recent efforts to close the gap between commonplace scripting languages and rarefied verification-integrated languages, enabling pathways to verified programming at every point along the spectrum from scripting languages to theorem proving languages.
Speaker Bio:
David Van Horn is an Assistant Professor in the Department of Computer Science and the Institute for Advanced Computer Studies (UMIACS) at the University of Maryland, College Park. His research interests are in programming languages and formal methods, where he works toward making the construction of reusable, trusted software components possible and effective. He publishes regularly in the flagship SIGPLAN conferences, POPL, PLDI, OOPSLA, and ICFP, and his work has been recognized with a National Science Foundation CAREER Award, a CRA Computing Innovation Fellowship, a Communications of the ACM Research Highlight, an OOPSLA Distinguished Paper Award, and several invitations to special issues of the Journal of Functional Programming devoted to ICFP. He is the co-author of "Realm of Racket," an illustrated book on programming video games, written and illustrated with eight undergraduate students. He is devoted to broadening participation in computer science and is currently serving as Chair of the ACM SIGPLAN Programming Languages Mentoring Workshop @ ICFP.
Notes:
In-person attendance only available to those with active NYU ID cards.