Defunctionalization with Dependent Types (PLDI 2023 - PLDI Research Papers) - PLDI 2023

Sat 17 - Wed 21 June 2023 Orlando, Florida, United States

Who

Yulong Huang, Jeremy Yallop

Track

PLDI 2023 PLDI Research Papers

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

Wed 21 Jun 2023 14:00 - 14:20 at Royal - PLDI: Types Chair(s): Benjamin Delaware

Abstract

The defunctionalization translation that eliminates higher-order functions from programs forms a key part of many compilers. However, defunctionalization for dependently-typed languages has not been formally studied.

We present the first formally-specified defunctionalization translation for a dependently-typed language and establish key metatheoretical properties such as soundness and type preservation. The translation is suitable for incorporation into type-preserving compilers for dependently-typed languages.

Link to Preprint

https://www.cl.cam.ac.uk/~jdy22/papers/defunctionalization-with-dependent-types.pdf

DOI

https://doi.org/10.1145/3591241

Yulong Huang

University of Cambridge

Jeremy Yallop

University of Cambridge

United Kingdom

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

Wed 21 Jun
Displayed time zone: Eastern Time (US & Canada) change

	13:40 - 15:40	PLDI: TypesPLDI Research Papers at Royal Chair(s): Benjamin Delaware Purdue University #pldi-wed-1340-types-royal

	13:40 20m Talk		Extensible Metatheory Mechanization via Family PolymorphismDistinguished Paper PLDI Research Papers Ende Jin University of Waterloo, Nada Amin Harvard University, Yizhou Zhang University of Waterloo DOI
	14:00 20m Talk		Defunctionalization with Dependent Types PLDI Research Papers Yulong Huang University of Cambridge, Jeremy Yallop University of Cambridge DOI Pre-print
	14:20 20m Talk		Garbage-Collection Safety for Region-Based Type-Polymorphic Programs PLDI Research Papers Martin Elsman University of Copenhagen, Denmark DOI
	14:40 20m Talk		Flux: Liquid Types for Rust PLDI Research Papers Nico Lehmann University of California, San Diego, Adam Geller Computer Science, University of British Columbia, Niki Vazou IMDEA Software Institute, Ranjit Jhala University of California at San Diego DOI
	15:00 20m Talk		Leveraging Rust Types for Program Synthesis PLDI Research Papers Jonas Fiala ETH Zürich, Shachar Itzhaky Technion, Peter Müller ETH Zurich, Nadia Polikarpova University of California at San Diego, Ilya Sergey National University of Singapore DOI Pre-print
	15:20 20m Talk		Parameterized Algebraic Protocols PLDI Research Papers Andreia Mordido LASIGE, University of Lisbon, Janek Spaderna University of Freiburg, Germany, Peter Thiemann University of Freiburg, Germany, Vasco T. Vasconcelos LASIGE, University of Lisbon DOI