[Pl-seminar] Reminder: Seminar TOMORROW: Max New: Call-By-Name Gradual Type Theory

[Daniel Patterson]

Reminder, this is tomorrow!

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.