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

This work introduces the novel concept of {\em kind refinement},
which we develop in the context of an explicitly
polymorphic ML-like language with type-level computation.
Just as type
refinements embed rich specifications by means of comprehension
principles expressed by predicates over values in the type domain,
kind refinements provide rich {\em kind} specifications by means of
predicates over {\em types} in the kind domain.
By leveraging our powerful refinement kind discipline, types in our
language are not just used to statically classify program
expressions and values, but also conveniently manipulated as
tree-like data structures, with their kinds refined by logical
constraints on such structures. Remarkably, the resulting typing
and kinding disciplines allow for powerful forms of type reflection,
ad-hoc polymorphism and type-directed meta-programming, which are
often found in modern software development, but not typically expressible in a
type-safe manner in general purpose languages.
We validate our approach both formally and pragmatically
by establishing the standard meta-theoretical results of type safety and
via a prototype implementation of a kind checker, type checker and
interpreter for our language.

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