- Mme Hariti
- bureau 5056
- 01 57 27 92 13
|Requirements||Classical Tools in parallel with this course will be a good complement.|
|Teacher||Alexis Saurin and Thomas Colcombet|
|Weekly hours||4 h CM|
|Years||Master Logique et Fondements de l'Informatique|
This course will study different aspects of the notion of second order in logic and will study fixed-point logics. In particular, various applications of these logical formalisms to the study of formal languages on words and trees and to the study of programming languages will be discussed.
-Syntax of second-order logic, natural second-order deduction, particular theories and fragments (PA2, HA2, MSO, F, ...).
-Second-order models: full models and Henkin models, second-order completeness.
-Proofs and programs: extension of the Curry-Howard correspondence (second-order and polymorphism) and study of the system F (definition, representation of data types, normalization theorems (Girard reducibility candidates, realizability), representative functions in F).
-Definitions, reminders and complements on the theory of automata.
-Decidability on words (Elgott-Büchi-Trakhtenbrot); links with automata and monoids.
-The first-order in the second-order (Schützenberger theorem).
-Decidability on tree-like structures (Courcelle's theorem) and structural bounds on decidability (Seese's theorem).
-The compositional method of Feferman-Vaught and Shelah.
-The theory of infinite words (Büchi, Safra).
-The theory of infinite trees and links with game theory (Rabin, Gurevitch and Harrington).
-Some results on fixed points.
-Syntaxes and semantics of logics with smaller and larger fixed points (inductive definitions à la Martin-Löf, mu-calculus for classical, intuitionistic and modal logics).
-Deduction systems for fixed-point logics: induction à la Park, Omega rule, circular proofs.
-Relations with automata, with monadic second-order logic.
-Completeness of the mu-calculus and other results.