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

In the context of gradual typing, type soundness guarantees the safety of typed
code. When untyped code fails to respect types, a runtime check finds the
discrepancy. As for untyped code, type soundness makes no promises; it
does not protect untyped code from mistakes in type specifications and
unwarranted blame.

To address the asymmetry, this paper adapts complete monitoring from the
contract world to gradual typing. Complete monitoring strengthens plain
soundness into a guarantee that catches problems with faulty type
specifications. Furthermore, a semantics that satisfies complete monitoring can
easily pinpoint the conflict between a type specification and a value. For
gradual typing systems that fail complete monitoring, the technical framework
provides a source-of-truth to assess the quality of blame.

Thu 24 Oct

Displayed time zone: Beirut change

16:00 - 17:30
TypesOOPSLA at Olympia
Chair(s): Éric Tanter University of Chile & Inria Paris
16:00
22m
Talk
Mergeable Replicated Data Types
OOPSLA
Gowtham Kaki Purdue University, Swarn Priya Purdue University, KC Sivaramakrishnan IIT Madras, Suresh Jagannathan Purdue University
Link to publication DOI
16:22
22m
Talk
Refinement Kinds: Type-Safe Programming with Practical Type-Level Computation
OOPSLA
Luís Caires Universidade Nova de Lisboa and NOVA LINCS, Bernardo Toninho Universidade Nova de Lisboa and NOVA LINCS
DOI
16:45
22m
Talk
System FR: Formalized Foundations for the Stainless Verifier
OOPSLA
Jad Hamza EPFL, Switzerland, Nicolas Voirol EPFL, Switzerland, Viktor Kunčak EPFL, Switzerland
DOI
17:07
22m
Talk
Complete Monitors for Gradual Types
OOPSLA
Ben Greenman PLT @ Northeastern University, Matthias Felleisen PLT @ Northeastern University, Christos Dimoulas PLT @ Northwestern University
DOI