Amortized Analysis of Splay Trees via a Lax Homomorphism (POPL 2026 - Student Research Competition) - POPL 2026

Sun 11 - Sat 17 January 2026 Rennes, France

Track

POPL 2026 Student Research Competition

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

When

Wed 14 Jan 2026 17:30 - 19:30 at Halle 0 - SRC Poster Session
Thu 15 Jan 2026 10:36 - 10:53 at Dortoirs - SRC Talks

Link to Preprint

https://lk672.github.io/popl26-src/extended-abstract.pdf

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

Session Program

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

	17:30 - 19:30	SRC Poster SessionStudent Research Competition at Halle 0

	17:30 2h Poster		AgdaGDL: A Geometric Deep Learning Framework for Property Certification Student Research Competition Mason Lary University at Buffalo, SUNY, Andrew K. Hirsch University at Buffalo, SUNY
	17:30 2h Poster		A Concise Type System for Borrow Inference Student Research Competition Tom Divers University of Bristol
	17:30 2h Poster		Language Model for MPI Student Research Competition Keith Allen University at Buffalo, SUNY, Andrew K. Hirsch University at Buffalo, SUNY
	17:30 2h Poster		An End-to-end Theory for Compositional Symbolic Execution: From Expressive Specifications to SMT Student Research Competition Shivanandan Tamil Kumaran Imperial College London
	17:30 2h Poster		RESpecBench: Rigorous Evaluation of Specification Generation with Automated Verification Student Research Competition Barış Bayazıt University of Toronto, Xujie Si University of Toronto
	17:30 2h Poster		Asymptotic Analysis as an Abstract Interpretation Student Research Competition Heewon Lee KAIST, Korea, South (The Republic of) Pre-print
	17:30 2h Poster		A specification for Agda Core’s unification algorithm for generic pattern matching Student Research Competition Ewen BROUDIN-CARADEC ENS Paris Saclay, TU Delft, INRIA Saclay, LMF Link to publication Pre-print
	17:30 2h Poster		Amortized Analysis of Splay Trees via a Lax Homomorphism Student Research Competition Lukas Kebuladze Carnegie Mellon University Pre-print
	17:30 2h Poster		Handling the Selection Monad, Uniformly Student Research Competition Akane Taniguchi Institute of Science Tokyo
	17:30 2h Poster		A Well-behaved Differentiable Logic Student Research Competition Jairo Miguel Marulanda-Giraldo University of Southampton
	17:30 2h Poster		Towards Functional Language Runtimes Without Garbage Collection Student Research Competition Dustin Juliano Indiana University Indianapolis
	17:30 2h Poster		The Expressiveness of Programs via Descriptive Complexity Student Research Competition Ziyue Jin Peking University
	17:30 2h Poster		Ariadne: Automatically Tuning Generator Weights Using Dynamic Sampling Student Research Competition Francille Zhuang Purdue University
	17:30 2h Poster		Specialisation: Context-Dependent Reasoning in Incorrectness Separation Logic Student Research Competition Raquel Fernandes da Silva Imperial College London, Sacha-Élie Ayoun Imperial College London, Azalea Raad Imperial College London, David Pichardie Meta
	17:30 2h Poster		A Verified Distributed Stream Processing Framework Student Research Competition Mathias Rabing Copenhagen University
	17:30 2h Poster		Partial Evaluation + Global Analyser = Separate Analyser Student Research Competition Gyuhyeok Oh Seoul National University
	17:30 2h Poster		Bootstrapping a Verified Compiler for an Imperative Language in Rocq Student Research Competition Kacper F. Korban EPFL
	17:30 2h Poster		Formally Verified Optimisations for the Pancake Compiler Student Research Competition Minh Do University of New South Wales
	17:30 2h Poster		Expanding Specification Capabilities of a Gradual Verifier with Pure Functions Student Research Competition Doruk Alp Mutlu Michigan State University
	17:30 2h Poster		Towards a Mechanised Theory of Fully Featured Compositional Symbolic Execution Student Research Competition Shivanandan Tamil Kumaran Imperial College London, Andreas Lööw Royal Holloway, University of London, Philippa Gardner Imperial College London
	17:30 2h Poster		RUXt: Automatic Compositional Type Safety Refutation Student Research Competition Pedro Carrott Imperial College London, Sacha-Élie Ayoun Imperial College London, Azalea Raad Imperial College London
	17:30 2h Poster		Save Time and Mechanize Student Research Competition George Zakhour University of St. Gallen
	17:30 2h Poster		Region Type System with Bidirectional Multiprompt Delimited Control Student Research Competition Alexander Phidias Goetz University of Tübingen
	17:30 2h Poster		Semantic Completeness of Higher-Order Probabilistic Separation Logics Student Research Competition Puming Liu New York University Shanghai
	17:30 2h Poster		Decompilation into Interaction Trees Student Research Competition Dao Le UNSW Sydney
	17:30 2h Poster		Interactive symbolic execution of concurrent programs in a theorem prover Student Research Competition Alexandre Pinazza EPFL
	17:30 2h Poster		Interrupt-Aware Variable Analysis for SSD Firmware Student Research Competition Hyeongseo Yoo Seoul National University and Samsung Electronics
	17:30 2h Poster		A theory of lists with combinators for SMT solvers Student Research Competition Pierre Goutagny Inria and University of Lille Pre-print

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

	10:20 - 12:00	SRC TalksStudent Research Competition at Dortoirs

	10:20 16m Poster		RESpecBench: Rigorous Evaluation of Specification Generation with Automated Verification Student Research Competition Barış Bayazıt University of Toronto, Xujie Si University of Toronto
	10:36 16m Poster		Amortized Analysis of Splay Trees via a Lax Homomorphism Student Research Competition Lukas Kebuladze Carnegie Mellon University Pre-print
	10:53 16m Poster		Semantic Completeness of Higher-Order Probabilistic Separation Logics Student Research Competition Puming Liu New York University Shanghai
	11:10 16m Poster		Language Model for MPI Student Research Competition Keith Allen University at Buffalo, SUNY, Andrew K. Hirsch University at Buffalo, SUNY
	11:26 16m Poster		Bootstrapping a Verified Compiler for an Imperative Language in Rocq Student Research Competition Kacper F. Korban EPFL
	11:43 16m Poster		An End-to-end Theory for Compositional Symbolic Execution: From Expressive Specifications to SMT Student Research Competition Shivanandan Tamil Kumaran Imperial College London

Lukas Kebuladze

Lukas Kebuladze

Carnegie Mellon University