Program
Wednesday September 10 2025
| Time | Session | Authors | Paper |
|---|---|---|---|
| 08:30-9:20 | 📑Registration | ||
| 09:20-9:30 | Opening | ||
| 09:30-10:30 | Invited Speaker (joint with LOPSTR) | Robbert Krebbers. TBA | chair: TBA |
| 10:30-11:00 | ☕️Coffee break | ||
| 11:00-12:00 | Session 1: Rewriting and Applications | Chair: TBA | |
| 11:00-11:30 | Anna Vitali, Roberto Amadini and Maurizio Gabbrielli. | Fixture Layout Optimization in Wood Industry: A Case Study. | |
| 11:30-12:00 | Gerald Whitters, Haoyun Qin, Boon Loo and Carolyn Talcott. | On the Automated Verification of BGP Convergence. | |
| 12:00-13:00 | 10 Year Most Influential Paper Award | TBA | TBA |
| 13:00-14:30 | 🥗Lunch break | ||
| 14:30-16:30 | Session 2: Rewriting | Chair: TBA | |
| 14:30-15:00 | Raúl López-Rueda, Duong Dinh Tran, Canh Minh Do, Santiago Escobar and Kazuhiro Ogata. | Folding Narrowing for the Analysis of Mutual Exclusion Protocols. | |
| 15:00-15:30 | Kanta Takahata, Jonas Schöpf, Naoki Nishida and Takahito Aoto. | Recovering Commutation of Logically Constrained Rewriting and Equivalence Transformations. | |
| 15:30-16:00 | Jan-Christoph Kassing, Leon Spitzer and Jürgen Giesl. | Dependency Pairs for Expected Innermost Runtime Complexity and Strong Almost-Sure Termination of Probabilistic Term Rewriting. | |
| 16:00-16:30 | Maribel Fernandez and Jose Meseguer. | Formalizing Languages with Binding Operators in Rewriting Logic. | |
| 16:30-17:00 | ☕️Coffee break | ||
| 17:00-18:30 | Session 3: Programming Languages and Concurrency | Chair: TBA | |
| 17:00-17:30 | Mart Lubbers and Tim Steenvoorden. | A Reflection on Task-Oriented Programming. | |
| 17:30-18:00 | Cinzia Di Giusto, Pascal Urso and Etienne Lozes. | Realisability and Complementability of Multiparty Session Types. | |
| 18:00-18:30 | Valentin Pasquale and Álvaro García-Pérez. | An interactive type checker for dependent types with general recursion (System Description). | |
| 18:30-21:00 | 🍽_Excursion & Social Dinner | TBA |
Thursday September 11 2025
| Time | Session | Authors | Paper |
|---|---|---|---|
| 08:30-9:30 | 📑Registration | ||
| 09:30-10:30 | Invited Speaker | Ugo Dal Lago. (TBA) | chair: TBA |
| 10:30-11:00 | ☕️Coffee break | ||
| 11:00-13:00 | Session 4: Programming Languages | Chair: TBA | |
| 11:00-11:30 | Kai-Oliver Prott and Michael Hanus. | Determinism Types for Functional Logic Programming. | |
| 11:30-12:00 | Benedikt M. Rips, Niek Janssen, Mart Lubbers and Pieter Koopman. | Shallowly Embedded Functions. | |
| 12:00-12:30 | Hamza Jaafar and Guilhem Jaber. | Operational Game Semantics for generative algebraic effects. | |
| 12:30-13:00 | Renato Neves, José Proença and Juliana Souza. | An adequate while-language for stochastic hybrid computation. | |
| 13:00-14:30 | 🥗Lunch break | ||
| 14:30-16:30 | Session 5: Logical Frameworks and Type Systems | Chair: TBA | |
| 14:30-15:00 | Anders Schlichtkrull and Morten Konggaard Schou. | Formalizing Weighted Pushdown Systems in Isabelle/HOL. | |
| 15:00-15:30 | Chase Johnson and Gopalan Nadathur. | Transporting Theorems about Typeability in LF Across Schematically Defined Contexts. | |
| 15:30-16:00 | Beniamino Accattoli, Dan Ghica, Giulio Guerrieri, Claudio Belo Lourenço and Claudio Sacerdoti Coen. | Closure Conversion, Flat Environments, and the Complexity of Abstract Machines. | |
| 16:00-16:30 | Alain Delaet, Sandrine Blazy and Denis Merigoux. | Abstract machines and small-step semantics: a winning ticket for proof automation? | |
| 16:30-17:00 | ☕️Coffee break | ||
| 17:00-17:30 | Closing session |
List of all accepted papers (in no particular order)
- Raúl López-Rueda, Duong Dinh Tran, Canh Minh Do, Santiago Escobar and Kazuhiro Ogata. Folding Narrowing for the Analysis of Mutual Exclusion Protocols.
- Anders Schlichtkrull and Morten Konggaard Schou. Formalizing Weighted Pushdown Systems in Isabelle/HOL.
- Mart Lubbers and Tim Steenvoorden. A Reflection on Task-Oriented Programming.
- Anna Vitali, Roberto Amadini and Maurizio Gabbrielli. Fixture Layout Optimization in Wood Industry: A Case Study.
- Kai-Oliver Prott and Michael Hanus. Determinism Types for Functional Logic Programming.
- Kanta Takahata, Jonas Schöpf, Naoki Nishida and Takahito Aoto. Recovering Commutation of Logically Constrained Rewriting and Equivalence Transformations.
- Jan-Christoph Kassing, Leon Spitzer and Jürgen Giesl. Dependency Pairs for Expected Innermost Runtime Complexity and Strong Almost-Sure Termination of Probabilistic Term Rewriting.
- Cinzia Di Giusto, Pascal Urso and Etienne Lozes. Realisability and Complementability of Multiparty Session Types.
- Chase Johnson and Gopalan Nadathur. Transporting Theorems about Typeability in LF Across Schematically Defined Contexts.
- Gerald Whitters, Haoyun Qin, Boon Loo and Carolyn Talcott. On the Automated Verification of BGP Convergence.
- Maribel Fernandez and Jose Meseguer. Formalizing Languages with Binding Operators in Rewriting Logic.
- Beniamino Accattoli, Dan Ghica, Giulio Guerrieri, Claudio Belo Lourenço and Claudio Sacerdoti Coen. Closure Conversion, Flat Environments, and the Complexity of Abstract Machines.
- Benedikt M. Rips, Niek Janssen, Mart Lubbers and Pieter Koopman. Shallowly Embedded Functions.
- Hamza Jaafar and Guilhem Jaber. Operational Game Semantics for generative algebraic effects.
- Valentin Pasquale and Álvaro García-Pérez. An interactive type checker for dependent types with general recursion (System Description).
- Alain Delaet, Sandrine Blazy and Denis Merigoux. Abstract machines and small-step semantics: a winning ticket for proof automation?
- Renato Neves, José Proença and Juliana Souza. An adequate while-language for stochastic hybrid computation.