Binary search—think positive (ICFP 2025 - JFP First Papers) - ICFP 2025

Sun 12 - Sat 18 October 2025 Singapore

co-located with ICFP/SPLASH 2025

Who

Alexander Dinges, Ralf Hinze

Track

ICFP 2025 JFP First Papers

This program is tentative and subject to change.

Time Zone

The program is currently displayed in (GMT+08:00) Perth.

Use conference time zone: (GMT+08:00) PerthSelect 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 15 Oct 2025 14:30 - 14:55 at Orchid West - Types and Specifications

Abstract

The setting is a tutorial on program verification in Agda.

DOI

https://doi.org/10.1017/S0956796825000061

Alexander Dinges

RPTU Kaiserslautern-Landau

Germany

Ralf Hinze

RPTU Kaiserslautern-Landau

Germany

This program is tentative and subject to change.

Time Zone

The program is currently displayed in (GMT+08:00) Perth.

Use conference time zone: (GMT+08:00) PerthSelect 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 15 Oct
Displayed time zone: Perth change

	13:40 - 15:20	Types and SpecificationsICFP Papers / JFP First Papers at Orchid West

	13:40 25m Talk		McTT: A Verified Kernel for a Proof Assistant ICFP Papers Junyoung Jang McGill University, Antoine Gaulin McGill University, Jason Z. S. Hu Amazon, Brigitte Pientka McGill University DOI Media Attached
	14:05 25m Talk		Linear Types with Dynamic Multiplicities in Dependent Type Theory (Functional Pearl) ICFP Papers Maximilian Doré University of Oxford DOI Pre-print
	14:30 25m Paper		Binary search—think positive JFP First Papers Alexander Dinges RPTU Kaiserslautern-Landau, Ralf Hinze RPTU Kaiserslautern-Landau DOI
	14:55 25m Talk		Teaching Software Specification (Experience Report) ICFP Papers Cameron Moy Northeastern University, Daniel Patterson Northeastern University DOI