The program includes invited and contributed talks. The electronic informal proceedings are available here.

(tentative) Schedule (as PDF):
All times are in the CEST time zone (UTC+2:00).

---

08:50 - 09:00 Welcome Session
09:00 - 10:00 Session 1: (Invited Talk). Chair: Santiago Escobar

• (09:00) Daniele Nantes-Sobrinho (Universidade de Brasília, Imperial College London). Frame Inference in Separation Logic via Associative-Commutative Matching

10:00 - 10:30 Session 2: (Undecidability). Chair: David M. Cerna

• (10:00) Serdar Erbatur, Andrew M. Marshall, Paliath Narendran, and Christophe Ringeissen. Undecidability of Static Equivalence in Leaf Permutative Theories

10:30 - 11:00 Coffee Break

11:00 - 12:30 Session 3: (Commutative Theories). Chair: Silvio Ghilardi

• (11:00) Christophe Ringeissen and Laurent Vigneron. Combined Abstract Congruence Closure for Associative or Commutative Theories
• (11:30) Daniella Santaguida and Daniele Nantes-Sobrinho. Nominal Commutative Narrowing (Work in progress)
• (12:00) Andrés Felipe González Barragán, David M. Cerna, Mauricio Ayala-Rincón, and Temur Kutsia. On Anti-Unification over Absorption, Associative, and Commutative Theories

12:30 - 14:00 Lunch Break

14:00 - 15:00 Session 4: (Invited Talk). Chair: Oliver Fernández Gil

• (14:00) George Metcalfe (University of Bern). Independence in Logic and Algebra

15:00 - 16:00 Session 5: (Permissive Nominals, Convexity). Chair: Temur Kutsia

• (15:00) Alexander Baumgartner. Towards a Well-Founded ≤ Relation for Permissive Nominal Terms
  (virtual presentation)
• (15:30) Josué A. Ruiz, Amir Masoumzadeh, Paliath Narendran, and Padmavathi Iyer. On Testing Convexity of 2DNF
  (virtual presentation)

16:00 - 16:30 Coffee Break

16:30 - 18:00 Session 6: (High-Order Unification, Types). Chair: to be announced...

• (16:30) David M. Cerna and Julian Parsert. One is all you need: Second-order Unification without First-order Variables
• (17:00) Jean-Pierre Jouannaud. Type Independent Unification of Higher-Order Patterns
• (17:30) Gabriela Ferreira, David M. Cerna, Mauricio Ayala-Rincón, and Temur Kutsia. Computing Generalizers over Intersection and Union Type Theories

18:00 - 18:15 Closing Session

---

• George Metcalfe (University of Bern). Independence in Logic and Algebra (abstract)
• Daniele Nantes-Sobrinho (Universidade de Brasília, Imperial College London). Frame Inference in Separation Logic via Associative-Commutative Matching (abstract)

• David M. Cerna and Julian Parsert. One is all you need: Second-order Unification without First-order Variables (paper)
• Jean-Pierre Jouannaud. Type Independent Unification of Higher-Order Patterns (paper)
• Alexander Baumgartner. Towards a Well-Founded ≤ Relation for Permissive Nominal Terms (paper)
• Christophe Ringeissen and Laurent Vigneron. Combined Abstract Congruence Closure for Associative or Commutative Theories (paper)
• Daniella Santaguida and Daniele Nantes-Sobrinho. Nominal Commutative Narrowing (Work in progress) (paper)
• Josué A. Ruiz, Amir Masoumzadeh, Paliath Narendran, and Padmavathi Iyer. On Testing Convexity of 2DNF (paper)
• Serdar Erbatur, Andrew M. Marshall, Paliath Narendran, and Christophe Ringeissen. Undecidability of Static Equivalence in Leaf Permutative Theories (paper)
• Andrés Felipe González Barragán, David M. Cerna, Mauricio Ayala-Rincón, and Temur Kutsia. On Anti-Unification over Absorption, Associative, and Commutative Theories (paper)
• Gabriela Ferreira, David M. Cerna, Mauricio Ayala-Rincón, and Temur Kutsia. Computing Generalizers over Intersection and Union Type Theories (paper)