Demo Data from EDBT 2026 / reviewers in the wild / expert
Titouan Leclercq
dblp:441/7390
· DBLP profile ↗
1ranked-venue papers
1as first author
1since 2021 · last 2026
0009-0008-4423-442XORCID · reported
Domains — the database's venue-derived domains; a paper can count in several
Theory of computation · 1 · 1 first-author · 1 since 2021
Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.
| Theoretical computer science
1 paper |
Logic in computer science · 100% |
Topics — the 4 heaviest of 4, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Logic in computer science › constructive mathematics
computational interpretation |
1.0 | 1 | 2026 | Oracles Just for Fan: A Robust Computational Interpretation of the Fan Theorem · LICS 2026 |
Logic in computer science
constructive mathematics |
1.0 | 1 | 2026 | Oracles Just for Fan: A Robust Computational Interpretation of the Fan Theorem · LICS 2026 |
Logic in computer science › constructive mathematics
realizability |
1.0 | 1 | 2026 | Oracles Just for Fan: A Robust Computational Interpretation of the Fan Theorem · LICS 2026 |
Logic in computer science › proof theory
reverse mathematics |
1.0 | 1 | 2026 | Oracles Just for Fan: A Robust Computational Interpretation of the Fan Theorem · LICS 2026 |
Methods — techniques the papers use, named apart from their topics
λ-calculus with oracles · 1.0evidenced frames · 1.0
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2026 | Oracles Just for Fan: A Robust Computational Interpretation of the Fan TheoremabstractFriedman-Simpson’s original program of reverse mathematics, as is also the case for most of standard mathematics, has been developed in classical subsystems of second-order arithmetic. As such, (classical) reverse mathematics presents various limitations from a constructive point of view, since for instance it is unable to distinguish between a statement and its contrapositive (e.g. dependent choice and the bar induction principles). The case of (Weak) Kőnig’s Lemma (WKL) and Fan Theorem (FT) is particularly interesting in that regard: while WKL is well-known to imply FT, and if constructivists like Brouwer rejected the former while admitting the latter, the converse implication has not been much studied for years. It is only recently that a growing enthusiasm for constructive reverse mathematics pushed towards a finer-grained analysis of the connection between such principles. In addition to intuitionistic reverse mathematics, the realizability approach to logical principles adds a computational meaning to purely logical statements. We follow this path to investigate the computational meaning of Brouwer’s Fan Theorem: building on recent work by Lubarsky and Rathjen, we first construct a realizability interpretation of higher-order logic validating FT while refuting WKL. This interpretation relies on a λ-calculus extended with oracles while preserving a notion of continuity for realizers. We then push this approach a step further to show the robustness of this realizability interpretation by identifying, in the abstract and general setting of evidenced frames, sufficient computational conditions entailing FT. Titouan Leclercq, Étienne Miquey |
LICS | 1 |