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.

Syllabus:

• 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.