This program is tentative and subject to change.

Tue 25 Aug 2026 10:30 - 10:48 at IP126 Auditorium - Types, Testing, and Data Structures Chair(s): Steve Zdancewic

We propose an implementation model for the evaluation of the weak lambda-calculus, which is invariant for both time and space complexity, in both call-by-name and call-by-value strategies. In other words, this models provides an implementation of any weak call-by-name or weak call-by-value lambda-calculus reduction sequence, whose time complexity is polynomial in the number of simulated beta-steps, and space complexity is linear in the size of the largest intermediate term. This solves in an elegant way the well-known tension between time-invariance and space-invariance in the lambda-calculus.

This program is tentative and subject to change.

Tue 25 Aug

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

10:30 - 12:00
Types, Testing, and Data StructuresICFP Papers at IP126 Auditorium
Chair(s): Steve Zdancewic University of Pennsylvania
10:30
18m
Talk
Inlining as a space optimization: a simple time- and space-invariant implementation of the weak lambda-calculusDistinguished PaperRemote
ICFP Papers
Thibaut Balabonski LMF, CNRS, Université Paris-Saclay
DOI
10:48
18m
Talk
First-Class Constrained Types: Elaboration, Type Inference, Approximation, and a Characterization of TerminationDistinguished Paper
ICFP Papers
Chun Kit Lam The Hong Kong University of Science and Technology (HKUST), Florent Ferrari-Dominguez ENS de Lyon, Lionel Parreaux HKUST (The Hong Kong University of Science and Technology)
DOI
11:06
18m
Talk
Programmable Property-Based TestingDistinguished Paper
ICFP Papers
Alperen Keles University of Maryland at College Park, Justine Frank University of Maryland, College Park, Ceren Mert University of Maryland, College Park, Harrison Goldstein University at Buffalo, SUNY, Leonidas Lampropoulos University of Maryland at College Park
DOI
11:24
18m
Talk
A Catenable, Splittable, Transient Sequence Data StructureDistinguished Paper
ICFP Papers
DOI
11:42
18m
Talk
Adapting the MVVM pattern to C++ frontends and Agda-based backendsJFP First Paper
ICFP Papers
Viktor Csimma Eötvös Loránd University, Eötvös József Collegium (Budapest, Hungary)
Link to publication DOI Pre-print
Hide past events