Familiarity with Natural Deduction (ND) calculi for propositional, first-order, intuitionistic and predicate logics and general knowledge regarding foundations of logics and mathematics (on the level of graduate philosophy students) is assumed, but the material will be recapped (and significantly extended) during the lecture anyway. Basic familiarity with programming can be helpful.

In this course, assuming a basic knowledge of logic and a certain level of proficiency, an invited faculty member experienced with the use of proof assistants in research and teaching, along with a faculty member from our school, will collaborate to teach the use of proof assistants as tools for theorem proving in classical and intuitionistic first-order and higher-order calculi. The importance of ensuring correctness of proofs has been increasingly recognized in mathematics: one of the most famous proponents of computer-based proof verification was the late Vladmir Voevodsky, a winner of the Fields Medal (often called the Nobel Prize of Mathematics). Moreover, thanks to the Curry-Howard correspondence, proving theorems can be seen as constructing programs in a dependently-typed programming language, with proof normalization being the logical counterpart of program execution. In other words, it is possible to use proof assistants to automatically optimize proofs. More importantly from a logician's point of view, proof assistants allowing the use of meta-programming tools known as tactics (such as Coq, Lean or Abella) can greatly automate proof search. This course combines lectures and exercises gradually introducing students familiar with natural deduction to the Curry-Howard correspondence, dependent type theories, proving-as-programming and competent use of proof assistants.

By the end of this course, students will be able to

1. Use Coq as a reasoning tool for intutionistic, classical, propositional and predicate logics
2. Write standard functional programs in Coq's underlying functional language (Gallina)
3. Mechanize metatheory of logical calculi using deep embeddings
4. Extract verified programs from formalizations of constructively proved results

The schedule below is tentative and subject to change, depending also on the background and needs of prospective participants.

P: an ordinary blackboard/slides based presentation
C: a Coq-based presentation, including an interactive exercise session
E: a standard exercise session

Lecture 1 (P). Introduction to Coq and proof assistants

Lecture 2 (P+E). Recap of ND systems for intuitionistic and classical logic (alternative notations such as Fitch-style andsequent-style). Towards Curry-Howard correspondence: Proof-term assignment. Normalization and first computationalinsights. The Brouwer-Heyting Kolmogorov interpretation of intuitionistic connectives.

Lecture 3-4 (C). Getting familiar with the Coq environment. First encounters with assisted theorem proving: shallowembedding of intuitionistic logic. Translating ND derivations into Coq theorems. A first glimpse at automation.Remarksregarding alternative tactic languages (ssreflect).

Lecture 5-6 (P). Logic vs. type theory: a crash course. Simply typed lambda calculus (STLC). Towards higher-order and dependent type theories. Some information about the lambda cube and basic metatheorems. The Curry-Howard correspondence in full glory.

Lecture 7-9 (P+C). From CoC to CIC: Inductive types. Recursion and induction in Coq. Coq as a programming language. Basic inductive types (booleans, natural numbers…) and polymorphic ones (lists). Logical connectives as inductive types. Predicativity and impredicativity. The special status of Prop in Coq. Reflection. More about tactics and automation.

Lecture 10 (C). Additional axioms: excluded middle, functional extensionality, uniqueness of identity proofs, proof irrelevance. Advanced derivations and superintuitionistic predicate logics (Kuroda axiom, constant domains…).

Lecture 11-13 (C). Deep embeddings: extended case studies on mechanizing chosen proof systems for non-classical logics and proving metatheorems in Coq. Possible examples from the invited lecturer's own work: formalizing Ruitenburg's Theorem (FiCS 2024), negative translations for intuitionistic modal logics (FSCD 2017). Comparison with recent work mechanizing G4ip-style calculi (Férée and van Gool, Shillito and coauthors).

Lecture 14-15 (P + C). Loose ends and glimpses beyond (depending on time left, participants' interest and background) : Coq's underlying type theory (pCuIC). MetaCoq: using Coq to analyze Coq's consistency. Other Coq frameworks for metaprogramming (Coq-Elpi, Mtac2, Ltac2…). Remarks regarding other proof assistants (Agda,Isabelle, Abella, Lean). Program extraction. Feedback. Concluding remarks.

Students will solve exercises during and after class. The nature of Coq-based lectures allows to blur the distinction between lectures and exercise sessions: The proof assistant can be thought of as each student's personal tutor (a perspective suggested by Benjamin Pierce and his Software Foundations material).

Prerequisites: Familiarity with Natural Deduction (ND) calculi for propositional, first-order, intuitionistic and predicate logics and general knowledge regarding foundations of logics and mathematics (on the level of graduate philosophy students) is assumed, but the material will be recapped (and significantly extended) during the lecture anyway. Basic familiarity with programming can be helpful.

Grading system: the note is determined by up to three Coq-based assignments.

[1] Online book "Software Foundations" http://www.cis.upenn.edu/~bcpierce/sf/

[2] Online books by Adam Chlipala: "Certified Programming with Dependent Types" http://adam.chlipala.net/cpdt/ and "Formal Reasoning About Programs" http://adam.chlipala.net/frap/

[3] Lectures on the Curry-Howard Isomorphism. Series: Studies in Logic and the Foundations of Mathematics. Morten Heine Sørensen, Pawel Urzyczyn

[4] Supplementary reading on the theory of programming: Types and Programming Languages. Benjamin C. Pierce, The MIT Press

[5] Supplementary reading on Coq: Interactive Theorem Proving and Program Development Coq'Art: The Calculus of Inductive Constructions. Series: Texts in Theoretical Computer Science. An EATCS Series. Bertot, Yves, Casteran, Pierre

[6] In addition, the lecture will be using material developed by the lecturer. Parts marked with "C" in the schedule will be essentially self-contained: the students will work with the proof script that, at the same time, will be the basis for the presentation.

The relevant reading list will be provided at the course.

この科目は出願の際に成績証明書の提出が必要です。

Students are expected to bring their own laptop computers to the course. The main instructor of the course is Dr. Tadeusz Litak (University of Erlangen-Nuremberg, https://www8.cs.fau.de/wp-content/uploads/staff/litak/)