Reading Group

As of January 1, 2015, this reading group is in hiatus.

The Reading Group on Fixed Points meets once every two weeks to discuss the intersection of fixed points and proof theory. The discussion format is explained below.

Calendar

1. Classes of recursive functions: the Grzegorczyk hierarchy
   • When: 14:00 on June 26, in the Salle Schützenberger
   • Main paper: section 3.5 of Ulrich Kohlenbach, “Applied Proof Theory: Proof Interpretations and their Use in Mathematics” (PDF, 515KiB). Exercise 11 and 12 at the end of chapter 3 are also assigned as discussion topics.
   • Supplemental: H. E. Rose, Subrecursion (DJVU, 1.8MiB)
   • Supplemental: R. W. Ritchie, Classes of Recursive Functions Based on Ackermann’s Function (PDF, 1.7MiB)
   • Pen: D. Ilik
   • Note: the above links to the papers will only work from saclay.inria.fr or polytechnique.fr machines.
2. Paco: A Coq Library for Parameterized Coinduction
   • When: June 6, 2014 in Salle Schützenberger
   • Main paper: Chung-Kil Hur et al, The power of parameterization in coinductive proof, POPL 2013
   • Pen: Chaudhuri
3. Recursion from Iteration
   • Tuesday, April 8, at 14:00 in the Salle Schützenberger
   • Main paper: Andrzej Filinski, “Recursion from Iteration“, LISP and Symbolic Computation, 1994
   • Pen: D. Ilik
4. FO+LO+LFP=PTIME and related results in Descriptive Complexity Theory
   • Thursday, March 27 at 10:30 in the Salle Schützenberger
   • Main paper: Chapter 3.1 of Martin Grohe’s, “Descriptive Complexity, Canonisation, and Definable Graph Structure Theory“
   • Supplemental material: Notes on a talk by Neil Immerman (PS)
   • Supplemental paper (one of the original papers): Neil Immerman, “Relational queries computable in polynomial time“, Information and Control, 1986 (send mail to Kaustuv if you can’t access the PDF)
   • Supplemental paper (the other original paper): Moshe Y. Vardi, “The complexity of relational query languages“, STOC 1982
   • Supplemental material: A gentle(r) introduction from a course by Anuj Dawar
   • Pen: A. Das
5. Least and Greatest Fixed Points in MALL (Sequent Calculus)
   • Monday, February 10, 14:00 in the Salle Schützenberger
   • Main paper: David Baelde, Least and Greatest Fixed Points in Linear Logic, ACM Transactions on Computational Logic 13(1), 2012.
   • Supplementary: David Baelde and Dale Miller, Least and greatest fixed points in linear logic, LPAR 2007
   • Pen: K. Chaudhuri

Reading Stack

These papers/topics have been suggested for the reading group and may be part of future meetings.

• Work on cyclic structures and traced monoidal categories. Examples:
  • Masahito Hasegawa, “Recursion from Cyclic Sharing: Traced Monoidal Categories and Models of Cyclic Lambda Calculi”, TLCA 1997
  • —, “On traced monoidal categories”, MSCS 2009

Format

• Every participant is expected to have read the main assigned paper(s) and to have a list of prepared “questions” before the meeting. A meeting will be convened only when there is “quorum”, meaning that more than floor(half the group) have indicated that they have read the main papers and wish to discuss them.
• A “question” can be about, but is not limited to, the assigned papers, the subject of the assigned papers, or relationships to other subjects or papers. “Questions” need not end with a question mark, but they should not be used to soapbox, nor to incite meandering discussions that do not increase the general comprehension of the assigned papers.
• Every group is led by a Holder of The Pen whose task at the start of the meeting is to gather and arrange all the “questions” on the board in a sensible order. The Holder is not expected to be an expert, merely to direct the meeting and most importantly to bring it to an end in a reasonable amount of time (1 to 1.5 hours).
• The last person to arrive at a meeting is required to ask the first “question”.
• Not every “question” needs to be answered in the meeting.
• Each meeting will end with the selection of the following session’s assigned papers. A Holder will be selected from volunteers, or based on an LRU algorithm.