LSFA — PROGRAM
Days: Saturday, 18 July 2026 Sunday, 19 July 2026
Saturday, 18 July 2026
09:00-10:30
Session 1
LSFA
Location:
C4.07
| 09:00-10:00 |
Linearisation of the Lambda-Calculus: A Road Trip (abstract) 60 min
1 Universidade do Porto
|
| 10:00-10:30 |
A Typing System for the Linear Lambda-Calculus in de Bruijn Notation (abstract) 30 min
1 Inria
2 Université de Lorraine
|
10:30-11:00
Coffee Break
LSFA
Location:
C4.07
11:00-12:30
Session 2
LSFA
Location:
C4.07
| 11:00-11:30 |
Linearising Explicit Substitutions using Intersection Types (abstract) 30 min
1 Universidade do Porto
|
| 11:30-12:00 |
Phase Semantic Cut-elimination for Intuitionistic Linear Logic with Least and Greatest Fixed Points (abstract) 30 min
1 Hokkaido University
2 University of Sheffield
|
| 12:00-12:30 |
A Logical 3-valued Semantics for Non-Deterministic Choice (abstract) 30 min
1 University of Urbino Carlo Bo
|
12:30-14:00
Lunch
LSFA
Location:
C4.07
14:00-16:00
Session 3
LSFA
Location:
C4.07
| 14:00-15:00 |
Not Your Average Session Types (abstract) 60 min
1 Universidade de Lisboa
|
| 15:00-15:30 |
Colimit-Based Composition of High-Level Computing Devices (abstract) 30 min
1 Lancaster University
|
| 15:30-16:00 |
MaudeTypedLog: A Typed Interpreter for Prolog in Maude (abstract) 30 min
1 VRAIN, Universitat Politècnica de València
2 Faculty of Science, University of Porto
|
16:00-16:30
Coffee Break
LSFA
Location:
C4.07
16:30-17:30
Session 4
LSFA
Location:
C4.07
| 16:30-17:00 |
Collusion Relations and their Applications to Balance Theory (abstract) 30 min
1 Université Jean Moulin Lyon 3
2 Université Sorbonne Paris Nord
|
| 17:00-17:30 |
Dynamic Logic with Parallel Operator for Verifying Communication Protocols (abstract) 30 min
1 Universidade Federal Fluminese
2 Universidade Federal do Rio de Janeiro
|
Sunday, 19 July 2026
09:00-10:30
Session 5
LSFA
Session Chair:
Location:
C4.07
| 09:00-10:00 |
A General Approach for SMT Proof Skeletons (abstract) 60 min
1 Universidade Federal de Minas Gerais
|
| 10:00-10:30 |
Efficient Decision Procedures for RNMatrix Semantics (abstract) 30 min
1 UNICAMP
2 Université Sorbonne Paris Nord
3 University College London
|
10:30-11:00
Coffee Break
LSFA
Location:
C4.07
11:00-12:30
Session 6
LSFA
Location:
C4.07
| 11:00-11:30 |
A Machine-checked Proof of Consistency for Impredicative Pure Type Systems (abstract) 30 min
1 Universidad ORT Uruguay
|
| 11:30-12:00 |
Templates in Rewriting Induction (abstract) 30 min
1 Radboud University
|
| 12:00-12:30 |
Computer Science as Infrastructure: the Spine of the Lean Computer Science Library (CSLib) (abstract) 30 min
1 Drexel University
2 University of Southern Denmark
|
12:30-14:00
Lunch
LSFA
Location:
C4.07
14:00-16:00
Session 7
LSFA
Session Chair:
Location:
C4.07
| 14:00-15:00 |
NuITP: An Inductive Theorem Prover for Maude (abstract) 60 min
1 Universidad Politécnica de Valencia
|
| 15:00-15:30 |
Multiparty Session Types for GDPR Purpose Compliance (abstract) 30 min
1 University of Cyprus
|
| 15:30-16:00 |
Basic Model Theory for Path Predicate Modal Logic (abstract) 30 min
1 CONICET and Universidad Nacional de Córdoba, Argentina
2 CONICET and Universidad de Buenos Aires, Argentina
3 IMDEA Software Institute, Spain
|
16:00-16:30
Coffee Break
LSFA
Location:
C4.07
16:30-18:00
Session 8
LSFA
Location:
C4.07
| 16:30-17:00 |
Robust Classification in ML: A Topological Semantics Approach (abstract) 30 min
1 TU Wien
|
| 17:00-17:30 |
From Dag-Like Proofs to Boolean Circuits in Lean (abstract) 30 min
1 Pontifícia Universidade Católica do Rio de Janeiro
2 Pontifícia Universidade Católica do Rio de Janeiro (PUC-Rio)
|
| 17:30-18:00 |
Business Meeting (abstract) 30 min
1 Universidade de Goiás
|