A Quick Look at Impredicativity (ICFP 2020 - Program) - ICFP 2020

Write a Blog >>

Thu 20 - Fri 28 August 2020

Who

Alejandro Serrano, Jurriaan Hage, Simon Peyton Jones, Dimitrios Vytiniotis

Track

ICFP 2020 ICFP Program

Time Zone

The program is currently displayed in (GMT-04:00) Eastern Time (US & Canada).

Use conference time zone: (GMT-04:00) Eastern Time (US & Canada)Select other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

When

Tue 25 Aug 2020 15:30 - 15:45 at ICFP NY 4 - New York 4 Chair(s): Stephanie Weirich
Wed 26 Aug 2020 03:30 - 03:45 at ICFP Asia 4 - Asia 4 Chair(s): Stephanie Weirich

Abstract

Type inference for parametric polymorphism is wildly successful, but has always suffered from an embarrassing flaw: polymorphic types are themselves not first class. We present Quick Look, a practical, implemented, and deployable design for impredicative type inference. To demonstrate our claims, we have modified GHC, a production-quality Haskell compiler, to support impredicativity. The changes required are modest, localised, and are fully compatible with GHC’s myriad other type system extensions.

Link to Preprint

https://www.microsoft.com/en-us/research/publication/a-quick-look-at-impredicativity/

DOI

https://doi.org/10.1145/3408971

Alejandro Serrano

47 Degrees, Spain

Netherlands

Jurriaan Hage

Utrecht University, Netherlands

Simon Peyton Jones

Microsoft, UK

Dimitrios Vytiniotis

DeepMind

United Kingdom

YouTube

Time Zone

The program is currently displayed in (GMT-04:00) Eastern Time (US & Canada).

Use conference time zone: (GMT-04:00) Eastern Time (US & Canada)Select other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Session Program

Tue 25 Aug
Displayed time zone: Eastern Time (US & Canada) change

	14:30 - 16:30	New York 4ICFP Program at ICFP NY 4 Chair(s): Stephanie Weirich University of Pennsylvania Public livestreams: YouTube, Bilibili (China)

	14:30 15m Talk		The Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Made Easy (Functional Pearl) ICFP Program Lionel Parreaux EPFL DOI Pre-print Media Attached
	14:45 15m Talk		Liquid Resource Types ICFP Program Tristan Knoth University of California at San Diego, USA, Di Wang Carnegie Mellon University, Adam Reynolds University of California, San Diego, Nadia Polikarpova University of California, San Diego, Jan Hoffmann Carnegie Mellon University DOI Media Attached
	15:00 15m Talk		Cosmo: A Concurrent Separation Logic for Multicore OCaml ICFP Program Glen Mével Inria, Université Paris-Saclay, CNRS, Laboratoire de recherche en informatique, Jacques-Henri Jourdan Universersité Paris Saclay, CNRS, LRI, François Pottier Inria, France DOI Media Attached
	15:15 15m Talk		Composing and Decomposing Op-Based CRDTs with Semidirect Products ICFP Program Matthew Weidner Carnegie Mellon University, Christopher Meiklejohn Carnegie Mellon University, Heather Miller Carnegie Mellon University DOI Media Attached
	15:30 15m Talk		A Quick Look at ImpredicativityDistinguished Paper ICFP Program Alejandro Serrano 47 Degrees, Spain, Jurriaan Hage Utrecht University, Netherlands, Simon Peyton Jones Microsoft, UK, Dimitrios Vytiniotis DeepMind DOI Pre-print Media Attached
	15:45 15m Talk		A Unified View of Modalities in Type Systems ICFP Program Andreas Abel Gothenburg University, Jean-Philippe Bernardy University of Gothenburg, Sweden DOI Media Attached
	16:00 15m Talk		Lower Your Guards: A Compositional Pattern-Match Coverage Checker ICFP Program Sebastian Graf Karlsruhe Institute of Technology, Simon Peyton Jones Microsoft, UK, Ryan Scott Galois, Inc. Link to publication DOI Media Attached
	16:15 15m Talk		Signature restriction for polymorphic algebraic effects ICFP Program Taro Sekiyama National Institute of Informatics, Takeshi Tsukada Chiba University, Japan, Atsushi Igarashi Kyoto University, Japan DOI Media Attached

Wed 26 Aug
Displayed time zone: Eastern Time (US & Canada) change

	02:30 - 04:30	Asia 4ICFP Program at ICFP Asia 4 Chair(s): Stephanie Weirich University of Pennsylvania Public livestreams: YouTube, Bilibili (China)

	02:30 15m Talk		The Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Made Easy (Functional Pearl) ICFP Program Lionel Parreaux EPFL DOI Pre-print Media Attached
	02:45 15m Talk		Liquid Resource Types ICFP Program Tristan Knoth University of California at San Diego, USA, Di Wang Carnegie Mellon University, Adam Reynolds University of California, San Diego, Nadia Polikarpova University of California, San Diego, Jan Hoffmann Carnegie Mellon University DOI Media Attached
	03:00 15m Talk		Cosmo: A Concurrent Separation Logic for Multicore OCaml ICFP Program Glen Mével Inria, Université Paris-Saclay, CNRS, Laboratoire de recherche en informatique, Jacques-Henri Jourdan Universersité Paris Saclay, CNRS, LRI, François Pottier Inria, France DOI Media Attached
	03:15 15m Talk		Composing and Decomposing Op-Based CRDTs with Semidirect Products ICFP Program Matthew Weidner Carnegie Mellon University, Christopher Meiklejohn Carnegie Mellon University, Heather Miller Carnegie Mellon University DOI Media Attached
	03:30 15m Talk		A Quick Look at ImpredicativityDistinguished Paper ICFP Program Alejandro Serrano 47 Degrees, Spain, Jurriaan Hage Utrecht University, Netherlands, Simon Peyton Jones Microsoft, UK, Dimitrios Vytiniotis DeepMind DOI Pre-print Media Attached
	03:45 15m Talk		A Unified View of Modalities in Type Systems ICFP Program Andreas Abel Gothenburg University, Jean-Philippe Bernardy University of Gothenburg, Sweden DOI Media Attached
	04:00 15m Talk		Lower Your Guards: A Compositional Pattern-Match Coverage Checker ICFP Program Sebastian Graf Karlsruhe Institute of Technology, Simon Peyton Jones Microsoft, UK, Ryan Scott Galois, Inc. Link to publication DOI Media Attached
	04:15 15m Talk		Signature restriction for polymorphic algebraic effects ICFP Program Taro Sekiyama National Institute of Informatics, Takeshi Tsukada Chiba University, Japan, Atsushi Igarashi Kyoto University, Japan DOI Media Attached