|
19-23 mai 2025 Aussois (France)
|
Description des coursSTARTING BLOCK: COURSE 0: Back to basics Abstract: This background course will serve as a school starter. We will review the basic concepts underlying the school subjects reviewing classic topics 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) Abstract: The modal μ-calculus extends propositional modal logic by quantifiers for inductive and co-inductive constructions and serves as a natural metalanguage for temporal and fixed point modal logics. The first syntactic characterisation of this logic was, in retrospect, a system of ill-founded proofs. Completeness of a finitary calculus materialised only as a consequence of an intricate analysis of the infinitary system. The median of these extremes are the cyclic proofs, ill-founded proofs whose infinite expression is confined to periodic patterns, that is, unfoldings of finite graphs into trees. Such proofs display many of the advantages of both formalisms. In the first lecture we will present modal mu-calculus. More specifically, we cover syntax and semantics; fixed point nesting; approximants and signatures; model checking game and tableaux. Building on these, in the second lecture, we will look at recent development of infinitary and cyclic proof systems for the modal mu-calculus and, time permitting, its applications.
COURSE 2: Basics of category theory, algebras and coalgebras by Farzad Jafarrahmani (Lagrange Center, France) and Daniela Petrișan (Université Paris Cité, France) Abstract: We begin by providing some background in category theory, including the definitions of categories, functors, and natural transformations. Various examples will be presented to illustrate each concept, some of which will be referenced later in the course. As we plan to explore recursion in category theory, we will also cover the notions of limits and colimits. Next, we will study the notion of algebra and coalgebra in category theory. We aim to clarify concepts such as coinduction, bisimulation, and behavioural equivalence.
Finally, we will discuss the relationship between mathematical logic and category theory, leading to the introduction of the Curry-Howard-Lambek correspondence. As an example, we will explore how intuitionistic logic is related to cartesian closed categories. Using the previously discussed examples, we will then introduce concrete models to demonstrate the denotational semantics of programming languages.
COURSE 3: Automata on infinite structures by Karoliina Lehtinen (CNRS, France) Abstract: The goal of this course is to introduce the foundations of automata over infinite words and trees, and highlights their relationship to logic, and in particular the modal mu-calculus.
COURSE 4: Circular and non wellfounded proofs: expressiveness and semantics
by Anupam Das (University of Birmingham, UK) Abstract: TBA
by Farzad Jafarrahmani (Lagrange Center, France) Abstract: Building on the Curry-Howard-Lambek correspondence introduced in the previous lecture, this section focuses on understanding induction and co-induction from this perspective. We begin by exploring the categorical semantics of various logics extended with induction and co-induction. The discussion starts with intuitionistic logic, followed by its refinement through linear logic. We will examine the categorical axiomatization of linear logic with fixed points of types and illustrate this axiomatization with concrete examples. Finally, we conclude by briefly discussing the semantics of recursion and co-recursion in type theory, as well as the semantics of circular proofs in logic.
FROM ABSTRACTIONS TO APPLICATIONS: COURSE 5: Higher-order languages, Categories and Automata
by Daniela Petrișan (Université Paris Cité, France) Abstract: In this course we explain how various forms of automata and their algorithms can be seen from a more abstract and unifying perspective, using category theory. We can think of an automaton as a machine that processes some input, according to its structure, such as words or trees, and produces some effect in some universe of output values, such as Boolean values, weights in an arbitrary semiring or words over some alphabet, etc. This leads us to regard automata as functors from an input category – describing the structure of the inputs – to some output category – describing the computational effect. We also discuss the relation between this approach and the coalgebraic modelling of automata.
by Paul-André Melliès (CNRS, France) Abstract: In this course I will explain the connections between linear logic, intersection types, regular languages, and higher-order automata. I will focus more specifically on the comonadic translation, inspired by linear logic and domain theory, which allows one to extend parity automata on infinite words and trees to higher-order automata on lambda-Y-terms and infinite lambda-terms with boundaries. I will also illustrate the course with examples coming from higher-order model checking of mixed inductive and coinductive properties on infinite trees and lambda-terms.
COURSE 6: Bisimulation and coinductive types in the Rocq proof assistant by Damien Pous (CNRS, France) and Yannick Zakowski (INRIA, France) Abstract: The Rocq proof assistant provides inductive and coinductive datatypes. However, while the former yield initial algebras, it is not generally the case that the later yield final coalgebras: we need to consider them modulo bisimilarity. During this course we will present tools that make it possible to work efficiently with bisimilarity (or any coinductive predicate), and show how to obtain final coalgebras from coinductive types.
Bring you computer: the course will be based on Rocq exercises.
COURSE 7: Software Verification via Fixed-Point Logics: Constraint Solving, Cyclic-Proof Search, and Strategy Synthesis
by Hiroshi Unno (Tohoku University, Japan) Abstract: This course covers software verification based on fixed-point logics. It explains how the verification problems of safety and liveness specifications for imperative, functional, and probabilistic programs can be reduced to the validity checking problem of fixed-point logic formulas. The course then introduces three approaches to solving the validity checking problem. The first approach reduces the problem to a constraint-solving problem over predicate variables and explores solutions using template-based synthesis. The second approach casts the problem as a proof search problem in a cyclic proof system, demonstrating how various existing software model-checking techniques can be understood in a unified manner as different strategies for proof search. The third approach is based on the game semantics of fixed-point logics and reduces the problem to synthesizing a winning strategy. I explain how a method for solving this problem can be derived by analyzing, organizing, and integrating existing software verification and game solving techniques within a unified primal-dual framework based on the concept of Lagrangians.
COURSE 8: Guarded recursive types by Daniel Gratzer (Aarhus University, Denmark) and Adrien Guatto (Université Paris Cité, France) Abstract: TBA |
| Personnes connectées : 2 | Flux RSS | Vie privée | Accessibilité |
|
