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) PRESENTER: Christophe Ringeissen |
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) PRESENTER: Niels van der Weide |
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) |