FSCD 2025: FORMAL STRUCTURES FOR COMPUTATION AND DEDUCTION
PROGRAM

Days: Tuesday, July 15th Wednesday, July 16th Thursday, July 17th Friday, July 18th

Tuesday, July 15th

View this program: with abstractssession overviewtalk overview

10:00-10:30Coffee Break
10:30-12:30 Session 2: Unification, Matching, Generalisation
10:30
Mechanized Undecidability of Higher-order beta-Matching (abstract)
11:00
Combining Generalization Algorithms in Regular Collapse-Free Theories (abstract)
11:30
The Unification Type of an Equational Theory May Depend on the Instantiation Preorder (abstract)
PRESENTER: Franz Baader
12:00
Knowledge Problems vs Unification and Matching: Dichotomy Results (abstract)
12:30-14:00Lunch Break
14:00-15:30 Session 3: Types
14:00
Coherent Tietze transformations of 1-polygraphs in homotopy type theory (abstract)
14:30
Impredicative Encodings of Inductive and Coinductive Types (abstract)
15:00
Substructural Parametricity (abstract)
PRESENTER: Frank Pfenning
15:30-16:00Coffee Break
16:00-17:00 Session 4: Concurrency Models
16:00
Categorical Continuation Semantics for Concurrency (abstract)
PRESENTER: Hugo Paquet
16:30
Higher-Dimensional Automata : Extension to Infinite Tracks (abstract)
Wednesday, July 16th

View this program: with abstractssession overviewtalk overview

10:00-10:30Coffee Break
10:30-12:30 Session 6: Lambda Calculus
10:30
Grading call-by-push-value, explicitly and implicitly (abstract)
11:00
The Cost of Skeletal Call-by-Need, Smoothly (abstract)
11:30
Quantitative Types for the Functional Machine Calculus (abstract)
12:00
What does it take to certify a conversion checker? (abstract)
12:30-14:00Lunch Break
14:00-15:30 Session 7: Rewriting
14:00
Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems (abstract)
PRESENTER: Emma Ahrens
14:30
An Innermost DP Framework for Constrained Higher-order Rewriting (abstract)
PRESENTER: Cynthia Kop
15:00
Completeness of the decreasing diagrams method for proving confluence of rewriting systems of the least uncountable cardinality (abstract)
15:30-16:00Coffee Break
16:00-17:00 Session 8: Complexity
16:00
Unifying Algebraic and Boolean Descriptive Complexity (abstract)
PRESENTER: Damiano Mazza
16:30
Branch Sequentialization in Quantum Polytime (abstract)
PRESENTER: Mário Silva
Thursday, July 17th

View this program: with abstractssession overviewtalk overview

10:00-10:30Coffee Break
10:30-12:30 Session 10: Program Analysis
10:30
A Zoo of Continuity Properties in Constructive Type Theory (abstract)
PRESENTER: Martin Baillon
11:00
On the Metric Nature of (Differential) Logical Relations (abstract)
PRESENTER: Naohiko Hoshino
11:30
Internal Effectful Forcing in System T (abstract)
12:00
An Expressive Trace Logic for Recursive Programs (abstract)
PRESENTER: Reiner Hähnle
12:30-14:00Lunch Break
Friday, July 18th

View this program: with abstractssession overviewtalk overview

10:00-10:30Coffee Break
10:30-12:30 Session 13: Linear Logic
10:30
Yeo’s Theorem for Locally Colored Graphs: the Path to Sequentialization in Linear Logic (abstract)
PRESENTER: Rémi Di Guardia
11:00
Linear logic using negative connectives (abstract)
11:30
Functorial Models of Differential Linear Logic (abstract)
PRESENTER: Morgan Rogers
12:00
Ohana trees and Taylor expansion for the λI-calculus (abstract)
PRESENTER: Rémy Cerda
12:30-14:00Lunch Break
14:00-15:30 Session 14: Algebraic and Categorical Models
14:00
From Partial to Monadic: Combinatory Algebra with Effects (abstract)
14:30
∞-categorical models of linear logic (abstract)
PRESENTER: Elies Harington
15:00
Solving Guarded Domain Equations in Presheaves Over Ordinals and Mechanizing It (abstract)
15:30-16:00Coffee Break
16:00-17:00 Session 15: Logic
16:00
Interpolation as Cut-Introduction: On the Computational Content of Craig-Lyndon Interpolation (abstract)
16:30
Monad Translations for Higher-Order Logic (abstract)