**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

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

**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

**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

**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

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