LFMTP — PROGRAM
Days: Friday, 24 July 2026
Friday, 24 July 2026
09:00-10:00
Invited talk
LFMTP
Session Chair:
Location:
C5.02
| 09:00-10:00 |
It’s the End of the World as We Know It, and I Feel Funny (abstract) 60 min
1 University of Milan.
|
10:00-10:30
Coffee Break
LFMTP
Location:
C5.02
10:30-12:00
Unification
LFMTP
Session Chair:
Location:
C5.02
| 10:30-11:00 |
Anti-Unification Completeness Analysis in PVS (abstract) 30 min
1 Universidade de Brasília
2 Universidade Federal de Goiás
3 RISC
4 Johannes Kepler Universität
|
| 11:00-11:30 |
Formalizing Calculi with Unconventional Substitution (abstract) 30 min
1 Departamento de Matemática, Universidade do Minho, Portugal
2 Centro de Matemática da Universidade do Minho, Portugal
|
| 11:30-12:00 |
Work-in-Progress: A Tactic for Pattern Matching in Autosubst (abstract) 30 min
1 Heriot-Watt University Edinburgh
|
12:00-14:00
Lunch
LFMTP
Location:
C5.02
14:00-15:00
Calculi
LFMTP
Session Chair:
Location:
C5.02
| 14:00-14:30 |
Barbed Similarity for the $\pi$-Calculus in Beluga: A Case Study in Coinductive Reasoning (abstract) 30 min
1 Università degli Studi di Milano
2 Augusta University
|
| 14:30-15:00 |
A Strategy Language for Controlled Proof Search (abstract) 30 min
1 LIRMM, Univ Montpellier, CNRS
|
15:00-15:30
Coffee Break
LFMTP
Location:
C5.02
15:30-16:30
Quantification
LFMTP
Session Chair:
Location:
C5.02
| 15:30-16:00 |
Towards Generic Semantics for Substructural Generic Quantification (abstract) 30 min
1 Univ Rennes, CNRS, IRISA
|
| 16:00-16:30 |
Proof Theory and Dependent Type Theory: Distinct Foundations for Designing Proof Assistants (abstract) 30 min
1 Inria Saclay
|