POPL 2017
Sun 15 - Sat 21 January 2017
Fri 20 Jan 2017 10:55 - 11:20 at Auditorium - Type Systems 3 Chair(s): Derek Dreyer

While type soundness proofs are taught in every graduate PL class, the gap between realistic languages and what is accessible to formal proofs is large. In the case of Scala, it has been shown that its formal model, the Dependent Object Types (DOT) calculus, cannot simultaneously support key metatheoretic properties such as environment narrowing and subtyping transitivity, which are usually required for a type soundness proof. Moreover, Scala and many other realistic languages lack a general substitution property.

The first contribution of this paper is to demonstrate how type soundness proofs for advanced, polymorphic, type systems can be carried out with an operational semantics based on high-level, definitional interpreters, implemented in Coq. We present the first mechanized soundness proofs in this style for System F<: and several extensions, including mutable references. Our proofs use only straightforward induction, which is significant, as the combination of big-step semantics, mutable references, and polymorphism is commonly believed to require coinductive proof techniques.

The second main contribution of this paper is to show how DOT-like calculi emerge from straightforward generalizations of the operational aspects of F<:, exposing a rich design space of calculi with path-dependent types inbetween System F and DOT, which we dub the System D Square.

By working directly on the target language, definitional interpreters can focus the design space and expose the invariants that actually matter at runtime. Looking at such runtime invariants is an exciting new avenue for type system design.

Fri 20 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:10: Type Systems 3POPL at Auditorium
Chair(s): Derek DreyerMPI-SWS
10:30 - 10:55
Andrej DudenhefnerTechnical University Dortmund, Jakob RehofTechnical University Dortmund
10:55 - 11:20
Nada AminEPFL, Tiark RompfPurdue University
11:20 - 11:45
Carlo AngiuliCarnegie Mellon University, Robert Harper, Todd WilsonCalifornia State University Fresno
11:45 - 12:10
Stephen ChangNortheastern University, Alex KnauthNortheastern University, Ben GreenmanNortheastern University