Chaque année depuis 1973, l'École de Printemps d'Informatique Théorique constitue une école intensive dans un domaine de l'informatique théorique réunissant des universitaires confirmés comme de jeunes chercheuses et jeunes chercheurs. L'EPIT 2025 abordera une thématique issue de la logique, le raisonnement coinductif et circulaire, et ses applications en programmation, preuves formelles et vérification logicielle.
Étant donné le caractère très répandu des données définies inductivement (entiers, listes et arbres finies, etc.), l’induction est l’un des concepts fondamentaux de l’informatique et les principes d’induction sont parmi ses plus importants principes de raisonnements. En tant que concept dual de l’induction, la coinduction permet de modéliser et de raisonner sur les données et les comportements infinis (listes finies ou infinies, mots infinis, flots, arbres infinis, traces d’exécution, bisimulations, etc.) et s’accompagne de ses propres principes de raisonnement. Alors que la coinduction peut raisonnablement être considérée comme ayant le même caractère fondamental que l’induction, ce concept n’est pas aussi répandu dans la communauté d’informatique théorique que l’induction, ni aussi bien connu: l’attention portée à la coinduction est plus récente et la communauté informatique est loin d’être aussi familière avec la coinduction qu’avec l’induction.
Des formes variées de raisonnements inductifs et coinductifs ont été développées depuis le début du siècle, notamment le « raisonnement circulaire » logiquement fondé et apparenté au raisonnement par descente infinie initialement popularisé par Fermat en mathématiques. Notre projet, avec cette école est d’étudier les possibilités d’application de ces nouvelles formes de raisonnement (co)inductif — et notamment les preuves circulaires qui constituent une forme correcte de raisonnement circulaire — pour (i) les langages de programmation typés, (ii) les assistants de preuves et (iii) les techniques de vérification logicielles, de manière à mettre en évidence la convergence des méthodes de ces champs variés qui sont pourtant généralement conçus comme distincts.
Cette thématique vise en particulier à rassembler des membres issues de ces trois communautés pour mettre en évidence des perspectives communes et, si possible, faire émerger des intérêts de recherche communs. Pour prendre en compte la diversité du public visé, l'école débutera pas une demi-journée de "remise" à niveau visant à rappeler les bases de ces domaines avant d'en explorer les concepts et outils fondamentaux et de voir, dans une troisième partie, quelques perspectives plus avancées.
L'inscription à l'EPIT ouvrira le 31 janvier 2025.
Programme
Ce programme est prévisionnel: les titres des cours pourront évoluer lors de la publication des résumés des cours d'ici la fin février.
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 automataby 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)
Chargement... 
