log in  |  register  |  feedback?  |  help  |  web accessibility
PLunch: Let Arguments Go First
Yiyun Liu
Tuesday, November 26, 2019, 11:00 am-12:00 pm Calendar
  • You are subscribed to this talk through .
  • You are watching this talk through .
  • You are subscribed to this talk. (unsubscribe, watch)
  • You are watching this talk. (unwatch, subscribe)
  • You are not subscribed to this talk. (watch, subscribe)

Weekly PL reading group discussing the paper "Let Arguments Go First". Discussion will be led by Yiyun Liu. Paper available at https://link.springer.com/chapter/10.1007/978-3-319-89884-1_10

Bi-directional type checking has proved to be an extremely useful and versatile tool for type checking and type inference. The conventional presentation of bi-directional type checking consists of two modes: inference mode and checked mode. In traditional bi-directional type-checking, type annotations are used to guide (via the checked mode) the type inference/checking procedure to determine the type of an expression, and type information flows from functions to arguments.

This paper presents a variant of bi-directional type checking where the type information flows from arguments to functions. This variant retains the inference mode, but adds a so-called application mode. Such design can remove annotations that basic bi-directional type checking cannot, and is useful when type information from arguments is required to type-check the functions being applied. We present two applications and develop the meta-theory (mostly verified in Coq) of the application mode.

This talk is organized by Sankha Narayan Guria