Expressive static typing disciplines are a powerful way to achieve high-quality software. However, the adoption cost of such techniques should not be under-estimated. Just like gradual typing allows for a smooth transition from dynamically-typed to statically-typed programs, it seems desirable to support a gradual path to certified programming. We explore gradual certified programming in Coq, providing the possibility to postpone the proofs of selected properties, and to check “at runtime” whether the properties actually hold. Casts can be integrated with the implicit coercion mechanism of Coq to support implicit cast insertion à la gradual typing. Additionally, when extracting Coq functions to mainstream languages, our encoding of casts supports lifting assumed properties into runtime checks. Much to our surprise, it is not necessary to extend Coq in any way to support gradual certified programming. A simple mix of type classes and axioms makes it possible to bring gradual certified programming to Coq in a straightforward manner.

Tue 27 Oct
Times are displayed in time zone: Eastern Time (US & Canada) change

10:30 - 12:00
Session 2, Formalization, Semantics, and Static AnalysisDLS at Grand Station 3
10:30
22m
Talk
A Formalization of Typed Lua
DLS
Media Attached
10:52
22m
Talk
Gradual Certified Programming in Coq
DLS
Éric TanterUniversity of Chile, Chile, Nicolas TabareauInria
11:15
22m
Talk
Message Safety in Dart
DLS
Erik Ernst, Mathias SchwarzUber Aarhus, Fabio StroccoAarhus University, Denmark, Anders MøllerAarhus University
11:37
22m
Talk
Control-Flow Analysis of Dynamic Languages via Pointer Analysis
DLS
Steven Lyde, Matthew MightUniversity of Utah, USA, William E. Byrd