This reading group takes place on Friday from 1 pm to 3 pm at IRIF (To be announced) twice per month. Its aim is to understand inductive and circular proofs and also studying their semantic.

Planning 2019:

• 11/10/2019: Farzad Jafarrahmani. Denotational Semantics of Linear Logic with Least and Greatest Fixpoints. Slides.

• 8/11/2019: Felix Castro. Induction and co-induction in Martin-Löf type theory based on [14] and [15]. Slides.

• 15/11/2019: Farzad Jafarrahmani. Induction in the Fibred Multicategory. Slides.

• 13/12/2019: Abhishek De. [13], [17], [18], [19]. Slides.

Planning 2020:

• 07/03/2020: Abhishek De. The parallel syntax of non-wellfounded proof theory [5]. Slides.

• ?

References:

• [1] FARZANEH DERAKHSHAN AND FRANK PFENNING. CIRCULAR PROOFS AS SESSION-TYPED PROCESSES:A LOCAL VALIDITY CONDITION.

• [2] Robert Atkey, Patricia Johann, and Neil Ghani. When Is a Type Refinement an Inductive Type?

• [3] Pierre-Evariste, DagandConor McBride. A Categorical Treatment of Ornaments.

• [4] Claudio Hermida, Bart Jacobs. Structural Induction and Coinduction ina Fibrational Setting.

• [5] Abhishek De, Alexis Saurin. Infinets: The Parallel Syntax for Non-wellfounded Proof-Theory.

• [6] Rémi Nollet, Alexis Saurin, Christine Tasson. Local Validity for Circular Proofs in Linear Logicwith Fixed Points.

• [7] James Brotherston, Alex Simpson. Sequent calculi for induction and infinite descent.

• [8] Stefano Berardi, Makoto Tatsuta. Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proofs.

• [9] Stefano Berardi, Makoto Tatsuta. Intuitionistic Podelski-Rybalchenko Theorem and Equivalence Between Inductive Definitions and Cyclic Proofs.

• [10] Stefano Berardi, Makoto Tatsuta. Equivalence of inductive definitions and cyclic proofs under arithmetic.

• [11] Bahareh Afshari, Gerhard Jager, Graham E. Leigh. An infinitary treatment of full mu-calculus.

• [12] Hugo Herbelin. A Constructive Proof of Dependent Choice,Compatible with Classical Logic.

• [13] Anupam Das, Damien Pous. A Cut-Free Cyclic Proof System for Kleene Algebra.

• [14] Thierry Coquand. Infinite Objects in Type Theory.

• [15] Eduardo Giménez. Structural recursive definitions in type theory.

• [16] Venanzio Capretta. Coalgebras in functional programming and typetheory.

• [17] Amina Doumane, Damien Pous. Completeness for Identity-free Kleene Lattices.

• [18] Anupam Das, Damien Pous. Non-wellfounded proof theory for (Kleene+action)(algebras+lattices).

• [19] Anupam Das, Amina Doumane, Damien Pous. Left-Handed Completeness for Kleene algebra, via Cyclic Proofs.

• [20] Yves Bertot. CoInduction in Coq.