Theoretical Computer Science

This course presents some of the fundamentals of computer science on its two paradigms of computation, namely reduction (calculation step by step) and resolution (logical inference / automatic reasoning).

Teaching time performed: 15 hours of tutorials and 3 hours of practical classes in Coq

Part of the teaching team for the school year 2021-2022.

Instructors: Marc Aiguier and Pascale Le Gall

Student level: Second year (~M1/MSc)

Part of this elective course overlaps with the courses Logic modeling and formal systems and Logic modeling and formal systems, mandatory courses for the computer science major in third year.


  • Induction and recurrence (well-founded sets, etc).
  • Computability (Gödel/Herbrand’s recursive functions, Turing machines and all the associated indecidability results).
  • Mathematical logic (syntax, semantics and proof systems). Propositional and first-order logics are be detailed.