Thu 8 Nov 2018 11:37 - 12:00 at Studio 2 - Types and Contracts Chair(s): Hakjoo Oh

Gradual typing has emerged as the tonic for programmers wanting a mixture of static and dynamic typing, hoping to achieve the best of both. Sound gradual typing is the most potent brew, providing static type-checking and dynamic assertions. Contracts provide a lightweight form of gradual typing as they can be implemented as a library, rather than requiring a gradual type system.

Intersection and union types are well suited to dynamic languages: intersection encodes overloaded functions; union encodes uncertain data arising from branching code. We extend the untyped lambda calculus with contracts for monitoring higher-order intersection and union types, giving a uniform treatment to both. Each operator requires a single reduction rule that does not depend on the constituent types, or the context of the operator, unlike existing work.

We present a new method for defining contract satisfaction based on blame behaviour. A value positively satisfies a type if applying a contract of that type can never elicit positive blame. A continuation negatively satisfies a type if applying a contract of that type can never elicit negative blame. We supplement our definition of satisfaction with a series of monitoring properties that satisfying values and continuations should have. These properties ensure that the semantics of contracts are in alignment with the static types they represent.

Thu 8 Nov
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

10:30 - 12:00: Types and ContractsOOPSLA at Studio 2
Chair(s): Hakjoo OhKorea University
10:30 - 10:52
Horn-ICE Learning for Synthesizing Invariants and Contracts
Deepak D'Souza, Ezudheen P, Pranav GargUniversity of Illinois at Urbana-Champaign, Daniel NeiderMax Planck Institute for Software Systems, P. MadhusudanUniversity of Illinois at Urbana-Champaign
10:52 - 11:15
Gradual Liquid Type InferenceDistinguished Paper Award
Niki VazouIMDEA Software Institute, √Čric TanterUniversity of Chile & Inria Paris, David Van HornUniversity of Maryland, USA
11:15 - 11:37
Collapsible Contracts: Fixing a Pathology of Gradual Typing
Daniel FelteyNorthwestern University, USA, Ben GreenmanNortheastern University, USA, Christophe ScholliersUniversiteit Gent, Belgium, Robby FindlerNorthwestern University, USA, Vincent St-AmourNorthwestern University
11:37 - 12:00
The Root Cause of Blame: Contracts for Intersection and Union Types
Jack WilliamsUniversity of Edinburgh, UK, J. Garrett MorrisUniversity of Kansas, USA, Philip WadlerUniversity of Edinburgh, UK