Every year since 1973, EPIT, the French Spring School on Theoretical Computer Science, consists in an intensive research school in a field of TCS which gathers senior academics as well as young researchers. EPIT 2025 will focus on a theme from logic, coinductive and circular reasoning, and its applications to programming, formal proofs and software verification.
Given the widespread nature of inductively defined data (integers, finite lists and trees, etc.), induction is one of the fundamental concepts in computer science, and the principles of induction are among its most important reasoning principles. As the dual concept of induction, coinduction allows for modeling and reasoning about infinite data and behaviors (finite or infinite lists, infinite words, streams, infinite trees, execution traces, bisimulations, etc.), and comes with its own reasoning principles.
While coinduction can reasonably be considered as fundamental as induction, this concept is not as widespread in the theoretical computer science community as induction, nor as well known: attention to coinduction is more recent, and the computer science community is far less familiar with coinduction than with induction.
Various forms of inductive and coinductive reasoning have been developed since the beginning of the century, including logically grounded "circular reasoning," related to infinite descent reasoning, initially popularized by Fermat in mathematics. Our project, with this school, is to explore the potential applications of these new forms of (co)inductive reasoning — and in particular circular proofs, which constitute a correct form of circular reasoning — for (i) typed programming languages, (ii) proof assistants, and (iii) software verification techniques, in order to highlight the convergence of methods from these diverse fields that are typically considered distinct.
This year topic aims at gathering members of those three communities to evidence shared perspectives and, if possible, foster the emergence of joint research interests. In order to take into account the diversity of the targeted audience, the school will start with half-a-day of lecture reviewing background of those domains recalling the prior knowledge, it will then explore the fundamental concepts and tools of the topic before, in a third part, providing more advanced research perspectives.
Registration will open on january 31st.
Program
This programme is provisional: titles of the courses may be updated as the syllabus of each course is published by the end of february.
STARTING BLOCK:
COURSE 0: Back to basics – Background course as a school starter. A review of the basic concepts underlying the school (in proof theory, type theory, verification and model-checking, fixed-points, coinductive reasoning, basics of proof assistants, etc.)
FUNDAMENTAL BLOCK:
COURSE 1: The μ-calculus and its proof-theory by Bahareh Afshari (University of Gothenburg, Sweden)
COURSE 2: Basics of category theory, algebras and coalgebras by Farzad Jafarrahmani (Lagrange Center, France) and Daniela Petrișan (Université Paris Cité, France)
COURSE 3: Automata on infinite structures by Karoliina Lehtinen (CNRS, France)
COURSE 4: Circular and non wellfounded proofs: expressiveness and semantics
Expressiveness of cyclic proofs by Anupam Das (University of Birmingham, UK)
Denotational semantics of (co)inductive types and fixed-point logics by Farzad Jafarrahmani (Lagrange Center, France)
FROM ABSTRACTIONS TO APPLICATIONS:
COURSE 5: Higher-order languages, Categories and Automata
Coalgebraic and functorial approaches to automata theory by Daniela Petrișan (Université Paris Cité, France)
Higher-order languages and automata by Paul-André Melliès (CNRS, France)
COURSE 6: Inductive and coinductive types in proof assistants by Damien Pous (CNRS, France) and Yannick Zakowski (INRIA, France)
COURSE 7: Cyclic-Proof Search for program verificationby Hiroshi Unno (Tohoku University, Japan)
COURSE 8: Guarded recursive types by Daniel Gratzer (Aarhus University, Denmark) and Adrien Guatto (Université Paris Cité, France)
Loading... 
