[Pl-seminar] CHANGED DATE: 4/27 Seminar: Max New: Call-By-Name Gradual Type Theory

[Daniel Patterson]

This seminar has been moved to a new date / time. It will now be next
FRIDAY, 4/27, at 11:30AM.

Daniel Patterson <dbp at ccs.neu.edu> writes:

> NUPRL Seminar Presents
>
> Max New
> Northeastern University
>
> 11:30AM
> Friday, April 27th, 2018
> Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)
>
> Call-By-Name Gradual Type Theory
>
> Abstract
>
> I will present Call-by-name (CBN) Gradual Type Theory [1], an
> axiomatic semantics of CBN gradual typing that directly axiomatizes
> the extensionality (eta) principles of types and the "gradual
> guarantee" of [2]. By axiomatizing the "term precision" relation
> of [2] we can provide a specification for casts as meets and joins
> with respect to precision. Using our type theory, we then show that
> the classic function contract ([3]) is in fact the unique
> implementation of function casts that satisfies extensionality and the
> gradual guarantee. This shows that the combination of these properties
> is a very strong constraint on the design of a gradually typed
> language and any implementation that departs must sacrifice one of
> these properties (typically extensionality).
>
> [1] Call-by-Name Gradual Type Theory, New and Licata, to appear FSCD '18,
> https://arxiv.org/abs/1802.00061
> [2] Refined Criteria for Gradual Typing, Siek, Vitousek, Cimini and
> Boyland, SNAPL '15, http://drops.dagstuhl.de/opus/volltexte/2015/5031/
> [3] Contracts for Higher-Order Functions, Findler and Felleisen, ICFP '02,
> https://dl.acm.org/citation.cfm?id=581484
>
> Bio
>
> Max New is a PhD student at Northeastern University working on the
> semantic foundations of programming languages. He hates proving the same
> theorem twice and you should too.