Program

PROGRAM

Days: Monday, July 3rd Tuesday, July 4th Wednesday, July 5th Thursday, July 6th

Monday, July 3rd

View this program: with abstracts session overview talk overview

09:00-10:00 Session 1: CADE-FSCD joint invited talk

Invited talk

Chair:

Cesare Tinelli

09:00

Mateja Jamnik

How Can We Make Trustworthy AI? (abstract)

10:00-10:30Coffee Break

10:30-12:30 Session 2

Chair:

Femke Van Raamsdonk

10:30	Lison Blondeau-Patissier, Pierre Clairambault and Lionel Vaux Auclair Strategies as Resource Terms, and their Categorical Semantics (abstract) PRESENTER: Lison Blondeau-Patissier
11:00	Nicolas Behr, Paul-André Melliès and Noam Zeilberger Convolution Products on Double Categories and Categorification of Rule Algebras (abstract) PRESENTER: Paul-André Melliès
11:30	James Laird Dinaturality meets genericity: a game semantics of bounded polymorphism. (abstract)
12:00	Rafaël Bocquet, Ambrus Kaposi and Christian Sattler For the Metatheory of Type Theory, Internal Sconing Is Enough (abstract) PRESENTER: Rafaël Bocquet

12:30-14:00Lunch Break

14:00-15:30 Session 3

Chair:

Herman Geuvers

14:00	Francesco Dagnino and Fabio Pasquali Quotients and Extensionality in Relational Doctrines (abstract) PRESENTER: Francesco Dagnino
14:30	Niels van der Weide The Formal Theory of Monads, Univalently (abstract)
15:00	Thorsten Altenkirch, Ambrus Kaposi, Artjoms Sinkarovs and Tamás Végh Combinatory logic and lambda calculus are equal, algebraically (abstract) PRESENTER: Ambrus Kaposi

15:30-16:00Coffee Break

16:00-20:00 Excursion

Excursion

20:00-23:00 Conference dinner

Conference dinner

Tuesday, July 4th

View this program: with abstracts session overview talk overview

09:00-10:00 Session 4: FSCD-CADE joint invited talk

invited talk

Chair:

Jürgen Giesl

09:00

Maribel Fernández

Nominal Techniques for Software Specification and Verification (abstract)

10:00-10:30Coffee Break

10:30-12:30 Session 5: Linear Logic

Chair:

Daniele Nantes-Sobrinho

10:30	Michele Pagani, Thomas Ehrhard and Claudia Faggian The Sum-Product Algorithm for Quantitative Multiplicative Linear Logic (abstract) PRESENTER: Michele Pagani
11:00	Flavien Breuvart, Marie Kerjean and Simon Mirwasser Unifying Graded Linear Logic and Differential Operators (abstract) PRESENTER: Simon Mirwasser
11:30	Rémi Di Guardia and Olivier Laurent Type Isomorphisms for Multiplicative Additive Linear Logic (abstract) PRESENTER: Rémi Di Guardia
12:00	Emmanuel Beffara, Félix Castro, Mauricio Guillermo and Étienne Miquey Concurrent Realizability on Conjunctive Structures (abstract) PRESENTER: Étienne Miquey

12:30-14:00Lunch Break

14:00-15:30 Session 6

Chair:

Ambrus Kaposi

14:00	Dan Ghica and George Kaye Rewriting modulo traced comonoid structure (abstract) PRESENTER: George Kaye
14:30	Samuel Mimram Categorical coherence from term rewriting systems (abstract)
15:00	Taichi Uemura Homotopy type theory as internal languages of diagrams of $\infty$-logoses (abstract)

15:30-16:00Coffee Break

16:00-18:00 Session 7

Chair:

Clemens Grabmayer

16:00	Serenella Cerrito, Valentin Goranko and Sophie Paillocher Partial model checking and partial model synthesis in LTL using a tableau-based approach (abstract) PRESENTER: Valentin Goranko
16:30	Didier Galmiche and Daniel Mery Labelled Tableaux for Linear Time Bunched Implication Logic (abstract) PRESENTER: Daniel Mery

Wednesday, July 5th

View this program: with abstracts session overview talk overview

09:00-10:00 Session 8: FSCD invited talk

invited talk

Chair:

Herman Geuvers

09:00

Giulio Manzonetto

A Lambda Calculus Satellite (abstract)

10:00-10:30Coffee Break

10:30-12:30 Session 9

Chair:

Aleksy Schubert

10:30	Samuel Frontull, Georg Moser and Vincent van Oostrom α-avoidance (abstract) PRESENTER: Samuel Frontull
11:00	Pablo Barenbaum and Cristian Sottile Two Decreasing Measures for Simply Typed Lambda-Terms (abstract) PRESENTER: Cristian Sottile
11:30	Simona Ronchi Della Rocca and Daniele Pautasso A quantitative version of simple types (abstract) PRESENTER: Daniele Pautasso
12:00	Ugo Dal Lago, Naohiko Hoshino and Paolo Pistone On the Lattice of Program Metrics (abstract) PRESENTER: Naohiko Hoshino

12:30-14:00Lunch Break

14:00-15:30 Session 10

Chair:

Luca Roversi

14:00	Valentin Blot Diller-Nahm bar recursion (abstract)
14:30	Anupam Das and Lukas Melgaard Cyclic proofs for (arithmetical) inductive definitions (abstract) PRESENTER: Lukas Melgaard
15:00	Sergey Goncharov Representing Guardedness in Call-by-Value (abstract)

15:30-16:00Coffee Break

16:00-18:00 Session 11

General Meeting FSCD

Chair:

Herman Geuvers

Thursday, July 6th

View this program: with abstracts session overview talk overview

09:00-10:00 Session 12: FSCD invited talk

Invited Talk

Chair:

Aart Middeldorp

09:00

Akihisa Yamada

Termination of Term Rewriting: Foundation, Formalization, Implementation, and Competition (abstract)

10:00-10:30Coffee Break

10:30-12:30 Session 13

Chair:

Pablo Barenbaum

10:30	Ievgen Ivanov Generalized Newman's Lemma for Discrete and Continuous Systems (abstract)
11:00	Saraid Dwyer Satterfield, Serdar Erbatur, Andrew M. Marshall and Christophe Ringeissen Knowledge Problems in Security Protocols: Going Beyond Subterm-Convergent Theories (abstract) PRESENTER: Andrew M. Marshall
11:30	Théo Losekoot, Thomas Genet and Thomas Jensen Automata-based verification of relational properties of functions over data structures (abstract) PRESENTER: Théo Losekoot
12:00	Nao Hirokawa and Aart Middeldorp Hydra Battles and AC Termination (abstract) PRESENTER: Nao Hirokawa

12:30-14:00Lunch Break

14:00-15:30 Session 14

Chair:

Femke Van Raamsdonk

14:00	Deivid Vale and Cynthia Kop Cost-Size Semantics for Call-by-Value Higher-Order Rewriting (abstract) PRESENTER: Deivid Vale
14:30	Nikolai Kudasov E-unification for Second-Order Abstract Syntax (abstract)
15:00	José Espírito Santo and Filipa Mendes The logical essence of compiling with continuations (abstract) PRESENTER: José Espírito Santo

15:30-16:00Closing Coffee Break