Nef - GiacoFest 2026

Venuele Couvent des Jacobins

Room nameNef

Floor0

Capacity400

Room InformationNo extra information available

Program

Time Zone

The program is currently displayed in (GMT+01:00) Brussels, Copenhagen, Madrid, Paris.

Use conference time zone: (GMT+01:00) Brussels, Copenhagen, Madrid, ParisSelect 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

Save

You're viewing the program in a time zone which is different from your device's time zone change time zone

Wed 14 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

08:50 - 09:00	Opening DayPOPL at Nef

08:50 10m Day opening		Welcome from the general chair POPL

09:00 - 10:00	KeynotePOPL at Nef +0min +0min Chair(s): Sandrine Blazy University of Rennes

09:00 60m Keynote		Medium-scale automation for proof assistants POPL Damien Pous CNRS

10:30 - 12:10	Functional Programming POPL at Nef Chair(s): Alex Rice University of Edinburgh

10:30 25m Talk		Domain-Theoretic Semantics for Functional Logic Programming POPL Eddie Jones University of Bristol, Samson Main University of Bristol, Celia Mengyue Li University of Bristol, Jonathan Marriott University of Bristol, Alex Kavvos University of Bristol DOI
10:55 25m Talk		Handling Scope Checks: A Comparative Framework for Dynamic Scope Extrusion Checks POPL Michael Lee University of Cambridge, UK, Ningning Xie University of Toronto, Oleg Kiselyov Tohoku University, Jeremy Yallop University of Cambridge DOI
11:20 25m Talk		Hyperfunctions: Communicating Continuations POPL Donnacha Oisín Kidney Imperial College London, Nicolas Wu Imperial College London DOI Pre-print
11:45 25m Talk		Lazy Linearity for a Core Functional Language POPL Rodrigo Mesquita Well-Typed LLP, Bernardo Toninho Instituto Superior Técnico - University of Lisbon DOI Pre-print

14:00 - 15:40	Types 1POPL at Nef Chair(s): Lionel Parreaux Hong Kong University of Science and Technology

14:00 25m Talk		Extensible Data Types with Ad-Hoc Polymorphism POPL Matthew Toohey University of Toronto, Yanning Chen University of Toronto, Ara Jamalzadeh University of Toronto, Ningning Xie University of Toronto DOI Pre-print
14:25 25m Talk		Let Generalization, Polymorphic Recursion, and Variable Minimization in Boolean-Kinded Type Systems POPL Joseph Zullo Purdue University DOI
14:50 25m Talk		Local Contextual Type Inference POPL Xu Xue University of Hong Kong, Chen Cui University of Hong Kong, Shengyi Jiang The University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong DOI
15:15 25m Talk		Typing Strictness POPL Daniel Sainati University of Pennsylvania, Joseph W. Cutler University of Pennsylvania, Benjamin C. Pierce University of Pennsylvania, Stephanie Weirich University of Pennsylvania DOI

16:10 - 17:25	Synthesis 1POPL at Nef Chair(s): Benjamin Delaware Purdue University

16:10 25m Talk		Accelerating Syntax-Guided Program Synthesis by Optimizing Domain-Specific Languages POPL Zhentao Ye Peking University, Ruyi Ji Peking University, Yingfei Xiong Peking University, Xin Zhang Peking University DOI
16:35 25m Talk		Inductive Program Synthesis by Meta-Analysis-Guided Hole Filling POPL Doyoon Lee Seoul National University, Woosuk Lee Hanyang University, Kwangkeun Yi Seoul National University DOI
17:00 25m Talk		Oriented Metrics for Bottom-Up Enumerative Synthesis POPL Roland Meyer TU Braunschweig, Jakob Tepe TU Braunschweig DOI

Thu 15 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

09:30 - 09:50	Jacobins Convent and its HistoryPOPL at Nef

09:30 20m Social Event		Jacobins Convent and its History POPL

10:20 - 12:00	Concurrency: Testing and VerificationPOPL at Nef Chair(s): Ramanathan S. Thinniyam Uppsala University

10:20 25m Talk		(TOPLAS) Will it Fit? Verifying Heap Space Bounds of Concurrent Programs under Garbage Collection POPL Alexandre Moine New York University, Arthur Charguéraud Inria, François Pottier Inria DOI
10:45 25m Talk		Verifying Almost-Sure Termination for Randomized Distributed Algorithms POPL Constantin Enea LIX, CNRS, Ecole Polytechnique, Rupak Majumdar MPI-SWS, Harshit Jitendra Motwani MPI-SWS, V.R. Sathiyanarayana MPI-SWS DOI
11:10 25m Talk		Zoo: A Framework for the Verification of Concurrent OCaml 5 Programs using Separation Logic POPL Clément Allain INRIA, Gabriel Scherer Université Paris Cité - Inria - CNRS DOI
11:35 25m Talk		The Complexity of Testing Message-Passing Concurrency POPL Zheng Shi National University of Singapore, Lasse Møldrup Aarhus University, Umang Mathur National University of Singapore, Andreas Pavlogiannis Aarhus University DOI Pre-print

14:00 - 15:40	Proof AssistantsPOPL at Nef Chair(s): Dmitriy Traytel University of Copenhagen

14:00 25m Talk		A Lazy, Concurrent Convertibility Checker POPL Nathanaëlle Courant OCamlPro, Xavier Leroy Collège de France - PSL University DOI
14:25 25m Talk		Canonicity for Indexed Inductive-Recursive Types POPL András Kovács University of Gothenburg and Chalmers University of Technology DOI
14:50 25m Talk		Coco: Corecursion with Compositional Heterogeneous Productivity POPL Jaewoo Kim Seoul National University, Yeonwoo Nam Seoul National University, Chung-Kil Hur Seoul National University DOI
15:15 25m Talk		Towards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by Equality Saturation POPL Marcus Rossel Barkhausen Institut; TU Darmstadt, Rudi Schneider TU Berlin, Thomas Koehler ICube Lab - CNRS - Université de Strasbourg, Michel Steuwer TU Berlin, Andrés Goens TU Darmstadt DOI Pre-print

16:10 - 17:00	Verified CompilationPOPL at Nef Chair(s): Clément Pit-Claudel EPFL

16:10 25m Talk		A Family of Sims with Diverging Interests POPL Nicolas Chappe CNRS - Verimag DOI
16:35 25m Talk		Endangered by the Language But Saved by the Compiler: Robust Safety via Semantic Back-Translation POPL Niklas Mück MPI-SWS, Aina Linn Georges Max Planck Institute for Software Systems (MPI-SWS), Derek Dreyer MPI-SWS, Deepak Garg MPI-SWS, Michael Sammler Institute of Science and Technology Austria DOI Pre-print

17:00 - 18:30	PC Chair's Report and Business MeetingPOPL at Nef

17:00 90m Meeting		PC Chair's Report and Business Meeting POPL

Fri 16 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

09:00 - 10:00	KeynotePOPL Student Research Competition / POPL at Nef +0min +0min Chair(s): Suresh Jagannathan Purdue University

09:00 60m Keynote		Hardware-Software Contracts for High Assurance with Applications to Side-Channel Security POPL Caroline Trippel Stanford University

10:30 - 12:10	Concurrency: Types, Logics, and LibrariesPOPL at Nef Chair(s): Robbert Krebbers Radboud University Nijmegen

10:30 25m Talk		All for One and One for All: Program Logics for Exploiting Internal Determinism in Parallel ProgramsDistinguished Paper POPL Alexandre Moine New York University, Sam Westrick New York University, Joseph Tassarotti New York University DOI
10:55 25m Talk		A Verified High-Performance Composable Object Library for Remote Direct Memory Access POPL Guillaume Ambal , George Hodgkins University of Colorado, Mark Madler University of Colorado, Gregory Chockler University of Surrey, Brijesh Dongol University of Surrey, Joe Izraelevitz University of Colorodo Boulder, Azalea Raad Imperial College London, Viktor Vafeiadis MPI-SWS DOI
11:20 25m Talk		DafnyMPI: A Dafny Library for Verifying Message-Passing Concurrent Programs POPL Aleksandr Fedchin Tufts University, Antero Mejr Tufts University, Hari Sundar Tufts University, Jeffrey S. Foster Tufts University DOI
11:45 25m Talk		TypeDis: A Type System for Disentanglement POPL Alexandre Moine New York University, Stephanie Balzer Carnegie Mellon University, Alex Xu Carnegie Mellon University, Sam Westrick New York University DOI Pre-print

14:00 - 15:40	Probabilistic ProgrammingPOPL at Nef Chair(s): Michele Pagani ENS Lyon

14:00 25m Talk		Optimising Density Computations in Probabilistic Programs via Automatic Loop Vectorisation POPL Sangho Lim KAIST, Hyoungjin Lim KAIST, Wonyeol Lee POSTECH, Xavier Rival Inria - CNRS - Ecole Normale Superieure de Paris - PSL University, Hongseok Yang KAIST DOI
14:25 25m Talk		Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and InvariantsDistinguished Paper POPL Noam Zilberstein Cornell University, Alexandra Silva Cornell University, Joseph Tassarotti New York University DOI
14:50 25m Talk		Probabilistic Programming with Vectorized Programmable InferenceRemote POPL McCoy Reynolds Becker MIT, Mathieu Huot MIT, George Matheos Massachusetts Institute of Technology, Xiaoyan Wang Massachusetts Institute of Technology, Karen Chung Massachusetts Institute of Technology, Colin Smith Massachusetts Institute of Technology, Sam Ritchie Massachusetts Institute of Technology, Rif A. Saurous Google, Alexander K. Lew Yale University, Martin C. Rinard Massachusetts Institute of Technology, Vikash K. Mansinghka Massachusetts Institute of Technology DOI
15:15 25m Talk		Tropical Mathematics and the Lambda-Calculus II: Tropical Geometry of Probabilistic Programming Languages POPL Davide Barbarossa University of Bath, Paolo Pistone Université Claude Bernard Lyon 1 DOI

16:10 - 17:25	Automata 2POPL at Nef Chair(s): Umang Mathur National University of Singapore

16:10 25m Talk		Counting and Sampling Traces in Regular Languages POPL Alexis de Colnet TU Wien, Kuldeep S. Meel University of Toronto, Umang Mathur National University of Singapore DOI Pre-print
16:35 25m Talk		Parametrised Verification of Intel-x86 Programs POPL Parosh Aziz Abdulla Uppsala University; Mälardalen University, Mohamed Faouzi Atig Uppsala University, Ahmed Bouajjani Université Paris Cité, K Narayan Kumar Chennai Mathematical Institute, Prakash Saivasan Institute of Mathematical Sciences DOI
17:00 25m Talk		General Decidability Results for Systems with Continuous Counters POPL A. R. Balasubramanian Technical University of Munich, Matthew Hague Royal Holloway University of London, Rupak Majumdar MPI-SWS, Ramanathan S. Thinniyam Uppsala University, Georg Zetzsche MPI-SWS DOI

Wed 14 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change


Room	8:00						30						9:00						30						10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30
Nef											POPL Opening Day		POPL Keynote																		POPL Functional Programming																																										POPL Types 1																										POPL Synthesis 1

Thu 15 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change


Room	9:00						30						10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30						18:00						30
Nef							POPL Jacobins Convent and its History										POPL Concurrency: Testing and Verification																																												POPL Proof Assistants																										POPL Verified Compilation										POPL PC Chair's Report and Business Meeting

Fri 16 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change


Room	9:00						30						10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30
Nef	POPL Student Research Competition + POPL Keynote																		POPL Concurrency: Types, Logics, and Libraries																																										POPL Probabilistic Programming																										POPL Automata 2

Wed 14 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change


Room	8:00			15			30			45			9:00			15			30			45			10:00			15			30			45			11:00			15			30			45			12:00			15			30			45			13:00			15			30			45			14:00			15			30			45			15:00			15			30			45			16:00			15			30			45			17:00			15			30			45
Nef											POPL Welcome from the general chair 08:50 - 09:00		POPL Medium-scale automation for proof assistants 09:00 - 10:00																		POPL Domain-Theoretic Semantics for Functional Logic Programming 10:30 - 10:55					POPL Handling Scope Checks: A Comparative Framework for Dynamic Scope Extrus ... 10:55 - 11:20					POPL Hyperfunctions: Communicating Continuations 11:20 - 11:45					POPL Lazy Linearity for a Core Functional Language 11:45 - 12:10																											POPL Extensible Data Types with Ad-Hoc Polymorphism 14:00 - 14:25					POPL Let Generalization, Polymorphic Recursion, and Variable Minimization in ... 14:25 - 14:50					POPL Local Contextual Type Inference 14:50 - 15:15					POPL Typing Strictness 15:15 - 15:40											POPL Accelerating Syntax-Guided Program Synthesis by Optimizing Domain-Speci ... 16:10 - 16:35					POPL Inductive Program Synthesis by Meta-Analysis-Guided Hole Filling 16:35 - 17:00					POPL Oriented Metrics for Bottom-Up Enumerative Synthesis 17:00 - 17:25

Thu 15 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change


Room	9:00			15			30			45			10:00			15			30			45			11:00			15			30			45			12:00			15			30			45			13:00			15			30			45			14:00			15			30			45			15:00			15			30			45			16:00			15			30			45			17:00			15			30			45			18:00			15			30			45
Nef							POPL Jacobins Convent and its History 09:30 - 09:50										POPL (TOPLAS) Will it Fit? Verifying Heap Space Bounds of Concurrent Progra ... 10:20 - 10:45					POPL Verifying Almost-Sure Termination for Randomized Distributed Algorithms 10:45 - 11:10					POPL Zoo: A Framework for the Verification of Concurrent OCaml 5 Programs us ... 11:10 - 11:35					POPL The Complexity of Testing Message-Passing Concurrency 11:35 - 12:00																													POPL A Lazy, Concurrent Convertibility Checker 14:00 - 14:25					POPL Canonicity for Indexed Inductive-Recursive Types 14:25 - 14:50					POPL Coco: Corecursion with Compositional Heterogeneous Productivity 14:50 - 15:15					POPL Towards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem ... 15:15 - 15:40											POPL A Family of Sims with Diverging Interests 16:10 - 16:35					POPL Endangered by the Language But Saved by the Compiler: Robust Safety via ... 16:35 - 17:00					POPL PC Chair's Report and Business Meeting 17:00 - 18:30

Fri 16 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change


Room	9:00			15			30			45			10:00			15			30			45			11:00			15			30			45			12:00			15			30			45			13:00			15			30			45			14:00			15			30			45			15:00			15			30			45			16:00			15			30			45			17:00			15			30			45
Nef	POPL Hardware-Software Contracts for High Assurance with Applications to Sid ... 09:00 - 10:00																		POPL Distinguished Paper All for One and One for All: Program Logics for Exploiting Internal Det ... 10:30 - 10:55					POPL A Verified High-Performance Composable Object Library for Remote Direct ... 10:55 - 11:20					POPL DafnyMPI: A Dafny Library for Verifying Message-Passing Concurrent Programs 11:20 - 11:45					POPL TypeDis: A Type System for Disentanglement 11:45 - 12:10																											POPL Optimising Density Computations in Probabilistic Programs via Automatic ... 14:00 - 14:25					POPL Distinguished Paper Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Cond ... 14:25 - 14:50					POPL Remote Probabilistic Programming with Vectorized Programmable Inference 14:50 - 15:15					POPL Tropical Mathematics and the Lambda-Calculus II: Tropical Geometry of P ... 15:15 - 15:40											POPL Counting and Sampling Traces in Regular Languages 16:10 - 16:35					POPL Parametrised Verification of Intel-x86 Programs 16:35 - 17:00					POPL General Decidability Results for Systems with Continuous Counters 17:00 - 17:25

Room information: Nef

Wed 14 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Thu 15 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Fri 16 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Wed 14 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

POPL

POPL

POPL

POPL

POPL

Thu 15 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

POPL

POPL

POPL

POPL

POPL

Fri 16 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

POPL Student Research Competition + POPL

POPL

POPL

POPL

Wed 14 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Thu 15 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Fri 16 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Tracks

Room information: Nef

Program Display Configuration

Wed 14 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change

Thu 15 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change

Fri 16 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change

Wed 14 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change

POPL

POPL

POPL

POPL

POPL

Thu 15 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change

POPL

POPL

POPL

POPL

POPL

Fri 16 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change

POPL Student Research Competition + POPL

POPL

POPL

POPL

Wed 14 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change

Thu 15 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change

Fri 16 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change

Wed 14 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Thu 15 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Fri 16 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Wed 14 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Thu 15 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Fri 16 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Wed 14 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Thu 15 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Fri 16 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change