POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France

Continuing the tradition of previous years, POPL 2026 will include a program of tutorials covering topics relevant to the POPL community. Please read the call for tutorials if you’re interested in presenting a tutorial on the tool or topic of your choice.

Dates

This program is tentative and subject to change.

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

Sun 11 Jan

Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

09:00 - 10:30
Creusot: Formal verification of Rust programsTutorials at Salle 12
09:00
90m
Tutorial
Creusot: Formal verification of Rust programs
Tutorials
Li-yao Xia LMF, Inria, Université Paris-Saclay, Jacques-Henri Jourdan CNR, LMF, Arnaud Golfouse Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, Laboratoire des méthodes formelles, 91190, Gif-sur-Yvette, France, Vincent Lafeychine Université Paris-Saclay
09:00 - 10:30
BINSEC: Adapting Symbolic Execution for Binary-level SecurityTutorials at Salle 14
09:00
90m
Tutorial
BINSEC: Adapting Symbolic Execution for Binary-level Security
Tutorials
Sébastien Bardin CEA LIST, University Paris-Saclay, Frédéric Recoules CEA, List, Yanis Sellami CEA, List, Univ. Grenoble Alpes
11:00 - 12:30
Creusot: Formal verification of Rust programsTutorials at Salle 12
11:00
90m
Tutorial
Creusot: Formal verification of Rust programs
Tutorials
Li-yao Xia LMF, Inria, Université Paris-Saclay, Jacques-Henri Jourdan CNR, LMF, Arnaud Golfouse Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, Laboratoire des méthodes formelles, 91190, Gif-sur-Yvette, France, Vincent Lafeychine Université Paris-Saclay
11:00 - 12:30
BINSEC: Adapting Symbolic Execution for Binary-level SecurityTutorials at Salle 14
11:00
90m
Tutorial
BINSEC: Adapting Symbolic Execution for Binary-level Security
Tutorials
Sébastien Bardin CEA LIST, University Paris-Saclay, Frédéric Recoules CEA, List, Yanis Sellami CEA, List, Univ. Grenoble Alpes
14:00 - 15:30
Verifying Probabilistic Programs Using Separation LogicTutorials at Salle 12
14:00
90m
Tutorial
Verifying Probabilistic Programs Using Separation Logic
Tutorials
Alejandro Aguirre Aarhus University, Simon Oddershede Gregersen New York University, Philipp G. Haselwarter Aarhus University
14:00 - 15:30
Discrete and continuous models for concurrent systemsTutorials at Salle 14
14:00
90m
Tutorial
Discrete and Continuous Models for Concurrent Systems: From Petri Nets to Directed Spaces
Tutorials
Uli Fahrenberg Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF
16:00 - 17:30
Verifying Probabilistic Programs Using Separation LogicTutorials at Salle 12
16:00
90m
Tutorial
Verifying Probabilistic Programs Using Separation Logic
Tutorials
Alejandro Aguirre Aarhus University, Simon Oddershede Gregersen New York University, Philipp G. Haselwarter Aarhus University
16:00 - 17:30
Discrete and continuous models for concurrent systemsTutorials at Salle 14
16:00
90m
Tutorial
Discrete and Continuous Models for Concurrent Systems: From Petri Nets to Directed Spaces
Tutorials
Uli Fahrenberg Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF

Mon 12 Jan

Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

09:00 - 10:30
Syntactically and Semantically Constraining LLMsTutorials at Salle 20
09:00
90m
Tutorial
Syntactically and Semantically Constraining LLMs with Guarantees using Structured LLM Generation
Tutorials
Sasa Misailovic University of Illinois at Urbana-Champaign, Gagandeep Singh University of Illinois at Urbana-Champaign; VMware Research, Shubham Ugare Meta, Debangshu Banerjee UIUC, Tarun Suresh , Adharsh Kamath UIUC
11:00 - 12:30
Syntactically and Semantically Constraining LLMsTutorials at Salle 20
11:00
90m
Tutorial
Syntactically and Semantically Constraining LLMs with Guarantees using Structured LLM Generation
Tutorials
Sasa Misailovic University of Illinois at Urbana-Champaign, Gagandeep Singh University of Illinois at Urbana-Champaign; VMware Research, Shubham Ugare Meta, Debangshu Banerjee UIUC, Tarun Suresh , Adharsh Kamath UIUC
14:00 - 15:30
A Guided Tour through Oxidized OCamlTutorials at Salle 19
14:00
90m
Tutorial
A Guided Tour through Oxidized OCaml
Tutorials
Gavin Gray Brown University, Anil Madhavapeddy University of Cambridge, UK, KC Sivaramakrishnan IIT Madras and Tarides, Will Crichton Brown University, Shriram Krishnamurthi Brown University, Chris Casinghino Jane Street, Richard A. Eisenberg Jane Street
14:00 - 15:30
Veil: Automated and Interactive Verification of Transition SystemsTutorials at Salle 20
14:00
90m
Tutorial
Veil: Automated and Interactive Verification of Transition Systems
Tutorials
George Pîrlea National University of Singapore, Qiyuan Zhao National University of Singapore
16:00 - 17:30
A Guided Tour through Oxidized OCamlTutorials at Salle 19
16:00
90m
Tutorial
A Guided Tour through Oxidized OCaml
Tutorials
Gavin Gray Brown University, Anil Madhavapeddy University of Cambridge, UK, KC Sivaramakrishnan IIT Madras and Tarides, Will Crichton Brown University, Shriram Krishnamurthi Brown University, Chris Casinghino Jane Street, Richard A. Eisenberg Jane Street
16:00 - 17:30
Veil: Automated and Interactive Verification of Transition SystemsTutorials at Salle 20
16:00
90m
Tutorial
Veil: Automated and Interactive Verification of Transition Systems
Tutorials
George Pîrlea National University of Singapore, Qiyuan Zhao National University of Singapore

Tue 13 Jan

Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

09:00 - 10:30
Analyzing Shell ScriptsTutorials at Salle 14
09:00
90m
Tutorial
Analyzing Shell Scripts
Tutorials
Michael Greenberg Stevens Institute of Technology, Konstantinos Kallas University of California, Los Angeles, Nikos Vasilakis Brown University
11:00 - 12:30
Analyzing Shell ScriptsTutorials at Salle 14
11:00
90m
Tutorial
Analyzing Shell Scripts
Tutorials
Michael Greenberg Stevens Institute of Technology, Konstantinos Kallas University of California, Los Angeles, Nikos Vasilakis Brown University
14:00 - 15:30
Is Program Synthesis Soluble in Large Language Models?Tutorials at Salle 14
14:00
90m
Tutorial
Is Program Synthesis Soluble in Large Language Models?
Tutorials
Nathanaël Fijalkow CNRS, LaBRI, University of Bordeaux
16:00 - 17:30
Is Program Synthesis Soluble in Large Language Models?Tutorials at Salle 14
16:00
90m
Tutorial
Is Program Synthesis Soluble in Large Language Models?
Tutorials
Nathanaël Fijalkow CNRS, LaBRI, University of Bordeaux

Unscheduled Events

Not scheduled
Talk
test1
Tutorials
Not scheduled
Talk
test2
Tutorials

Call For Tutorials

The 53rd ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2026) will be held in Rennes, France.

POPL provides a forum for the discussion of fundamental principles and important innovations in the design, definition, analysis, transformation, implementation, and verification of programming languages, programming systems, and programming abstractions.

Tutorials for POPL 2026 are solicited on any topic relevant to the POPL community. We particularly encourage submissions of introductory tutorials that make the research presented at POPL more accessible to the participants.

Tutorials will be held on Jan 11–13, 2026. The expected length of a tutorial is 3 hours, including questions and discussion (Q&A).

Submission details

  • Deadline for submission: October 10th, 2025
  • Notification of acceptance: October 24th, 2025

A tutorial proposal should provide the following information:

  • Tutorial title
  • Presenter(s), affiliation(s), and contact information
  • 1-3 page description (for evaluation). This should include the objectives, topics to be covered, presentation approach, target audience, prerequisite knowledge, and if the tutorial was previously held, the location (i.e. which conference), date, and number of attendees if available.
  • 1-2 paragraph abstract suitable for tutorial publicity.
  • 1-paragraph biography suitable for tutorial publicity.

Proposals must be submitted by email to Robert Rand (rand@uchicago.edu) and Alan Schmitt (alan.schmitt@inria.fr) with the subject line “POPL 2026 Tutorial Proposal: [tutorial name]”. The proposal should be attached as a PDF, docx, or txt file.

Further information

Any questions regarding POPL 2026 tutorials should be addressed to the workshops chairs, Robert Rand (rand@uchicago.edu) and Alan Schmitt (alan.schmitt@inria.fr).