Write a Blog >>
SPLASH 2019
Sun 20 - Fri 25 October 2019 Athens, Greece
Thu 24 Oct 2019 16:45 - 17:07 at Olympia - Types Chair(s): Éric Tanter

We present the design, implementation, and foundation of a verifier for higher-order functional programs with generics and recursive data types. Our system supports proving safety and termination using preconditions, postconditions and assertions. It supports writing proof hints using assertions and recursive calls. To formalize the soundness of the system we introduce System FR, a calculus supporting System F polymorphism, dependent refinement types, and recursive types (including recursion through contravariant positions of function types). Through the use of sized types, System FR supports reasoning about termination of lazy data structures such as streams. We formalize a reducibility argument using the Coq proof assistant and prove the soundness of a type-checker with respect to call-by-value semantics, ensuring type safety and normalization for typeable programs. Our program verifier is implemented as an alternative verification-condition generator for the Stainless tool, which relies on the Inox SMT-based solver backend for automation. We demonstrate the efficiency of our approach by verifying a collection of higher-order functional programs comprising around 14000 lines of polymorphic higher-order Scala code, including graph search algorithms, basic number theory, monad laws, functional data structures, and assignments from popular Functional Programming MOOCs.

Thu 24 Oct

splash-2019-oopsla
16:00 - 17:30: OOPSLA - Types at Olympia
Chair(s): Éric TanterUniversity of Chile & Inria Paris
splash-2019-oopsla16:00 - 16:22
Talk
Gowtham KakiPurdue University, Swarn PriyaPurdue University, KC SivaramakrishnanIIT Madras, Suresh JagannathanPurdue University
Link to publication DOI
splash-2019-oopsla16:22 - 16:45
Talk
Luís CairesUniversidade Nova de Lisboa and NOVA LINCS, Bernardo ToninhoUniversidade Nova de Lisboa and NOVA LINCS
DOI
splash-2019-oopsla16:45 - 17:07
Talk
Jad HamzaEPFL, Switzerland, Nicolas VoirolEPFL, Switzerland, Viktor KunčakEPFL, Switzerland
DOI
splash-2019-oopsla17:07 - 17:30
Talk
Ben GreenmanPLT @ Northeastern University, Matthias FelleisenPLT @ Northeastern University, Christos DimoulasPLT @ Northwestern University
DOI