FLoC'26 workshop, affiliated to FSCD'26
Place: Edifício II - ISCTE, Avenida das Forças Armadas, Lisbon, Portugal
Date: 18 July 2026
Registration: on the FLoC'26 website
Organizers: Frédéric Blanqui, Olivier Hermant and Pablo Arrighi
Gilles Dowek died on 21 July 2025 at 58 years old. He made important contributions not only in logic (unification, automated theorem proving, type theory) but also in quantum programming languages and philosophy. He received several awards from the French Academy of Sciences. He was a brilliant speaker and teacher and published several books in computer science, logic and philosophy. He has been very active in promoting the teaching of computer science in high school and contributed to the definition of the corresponding cursus. He also supervised or co-supervised many PhD students. Gilles Dowek published many papers in the FLoC conferences and workshops (LICS, RTA, TLCA, FSCD, TPHOL/ITP, LFMTP), served as PC chair of RTA-TLCA at FLoC'14, and has been a keynote speaker at IJCAR at FLoC’22.
This workshop aims at celebrating Gilles Dowek's influence in logic and computer science. We welcome talk proposals reviewing work done by Gilles or with him, or results obtained thanks to Gilles' influence or related to Gilles' work, that is, contributions exploring the connections between logics, computation, and possibly physical theories. Topics include, but are not limited to, logical frameworks, proof systems interoperability, ecumenical proof libraries, automated deduction, quantum programming languages, and physics-inspired models of computation. Submissions presenting results on the notion of universality across these domains are particularly encouraged. This workshop aims at paying tribute to the intellectual legacy of Gilles Dowek, whose work built bridges between these communities.
Original contributions are also invited to submit a paper to the coming TCS special issue on Universality in Logics and Physics dedicated to Gilles Dowek, and organized by Pablo Arrighi and Frank Pfenning.
Instructions: Provide an abstract of 2-3 pages max indicating the desired duration of the talk (15 or 30 minutes) and explaining the content of your talk.
Submission site: here
Important dates:
| Time | Speaker |
|---|---|
| 08:50 | |
| Introduction, Frédéric Blanqui and Olivier Hermant | |
| 09:00 | |
| On the Normative Power of Logical Frameworks, Frank Pfenning | |
| 09:30 | |
| Modeling and Proof Methods in Set Theory using Deduction Modulo Theory, Catherine Dubois and David Delahaye | |
| 10:00 | |
| Conservativity Made Easy, Thiago Felicissimo | |
| 10:30 | |
| coffee break | |
| 11:00 | |
| From Ecumenical Proof Theory to Automation, Elaine Pimentel and Luiz Carlos Pereira | |
| 11:30 | |
| Connecting Higher-Order Logics using Kolmogorov's Translation à la Dowek-Werner, Thomas Traversié | |
| 11:45 | |
| Parallel proof checking with short and long term memory, Michael Färber (online) | |
| 12:00 | |
| Theoretical and Practical Advances of Polarized Deduction Modulo Theory, Guillaume Burel | |
| 12:30 | |
| lunch | |
| 14:00 | |
| You Cannot Go Slower Than Your Speed, Cesar Muñoz (online) | |
| 14:30 | |
| Secure development of dependently typed programs using proxy-based small inversions, Pierre Corbineau, Basile Gros and Jean-François Monin | |
| 15:00 | |
| Compositional Pre-processing for Automated Reasoning in Dependent Type Theory, Valentin Blot | |
| 15:15 | |
| Reconstructing SMT Proofs in the λΠ/≡-calculus, Alessio Coltellacci | |
| 15:30 | |
| coffee break | |
| 16:00 | |
| Confluence of non-left-linear higher-order rewriting, Jean-Pierre Jouannaud | |
| 16:30 | |
| When Quantum Computing Challenges Logic, Alejandro Díaz-Caro | |
| 17:00 | |
| Explainability and the related issues in the digital-AI environments, Mitsuhiro Okada | |
| 17:30 | |
| I, Computer: Gilles’ Children’s Book on the Foundations of Computing, Nachum Dershowitz (online) |