Groupes pour rendre les rapports et les soutenances

Date	Rapports	Relecteurs	Relecteurs additionnels
12/1	Denis Kuperberg	Jonatan Lindén et Michal Palka
	Jonatan Lindén	Denis Kuperberg et Bertrand Marc
	Bertrand Marc	Jonatan Lindén et Michal Palka
	Michal Palka	Denis Kuperberg et Bertrand Marc
19/1	Laurent Boyer	Fanny Dufossé et Loïck Magnin	Denis Kuperberg
	Romain Demangeon	Fanny Dufossé et Loïck Magnin	Denis Kuperberg
	Fanny Dufossé	Laurent Boyer et Romain Demangeon	Bertrand Marc
	Loïck Magnin	Laurent Boyer et Romain Demangeon	Bertrand Marc
26/1	Thibaut Balabonski	Martin Delacourt et Ivan Morel
	Martin Delacourt	Thibaut Balabonski et Pierre Rannou
	Ivan Morel	Martin Delacourt et Pierre Rannou
	Pierre Rannou	Thibaut Balabonski et Ivan Morel
1/2?	Thomas Braibant	Vincent Nivoliers et Nicolas Perrin
	Vincent Nivoliers	Thomas Braibant et Nicolas Perrin
	Nicolas Perrin	Thomas Braibant et Vincent Nivoliers

Propositions d'articles à lire pour le cours "catégories en informatique et en logique" du M2IF de l'ENS Lyon.

Avertissement: je n'ai pas lu tous ces papiers, donc avant de vous arrêter sur l'un d'eux, tentez de deviner si vous allez réussir à le lire (par exemple, parcourez-le une fois). Ils sont de plus classés un peu artificiellement, donc ne vous limitez pas à une catégorie.

Le choix des papiers est à négocier. Venez me voir pour dire des trucs genre "j'aimerais bosser sur ça mais ce papier m'a l'air trop dur, je propose ça"...

Quantum

Pour approfondir les conneries que je vous ai racontées en cours. Le vrai truc c'est Selinger. Coecke c'est pour comprendre de haut. Baez c'est pour les oufs.

B. Coecke. Kindergarten Quantum Mechanics, 2005.

J. Baez. Quantum Quandaries: a Category-Theoretic Perspective.
Vincent Nivoliers?.

P. Selinger. Dagger compact closed categories and completely positive maps. Extended Abstract. To appear in Proceedings of the 3rd International Workshop on Quantum Programming Languages, Chicago, June 30 - July 1, 2005. 22 pages.
Loïck Magnin.

Catégories pures

J. Kock. Elementary remarks on units in monoidal categories. (Des petits trucs tout jolis sur la bonne définition des neutres dans les catégories monoïdales.)
Aline Parreau.

J. Baez. Universal Algebra and Diagrammatic Reasoning. (Un moyen d'approfondir l'aspect "une théorie équationnelle" = "une catégorie X initiale". Je vous conseille de suivre ce pointeur, qui peut compter à lui tout seul comme un papier à lire.)

Neil Ghani, Christoph Luth and Federico De Marchi. Monads of Coalgebras: Rational Terms and Term Graphs. Mathematical Structures in Computer Science.
Nicolas Perrin.

Un chapitre de
- Saunders Mac Lane. Categories for the Working Mathematician (2nd ed.). Graduate Texts in Mathematics 5. Springer, 1998. ISBN 0-387-98403-8.
- Saunders Mac Lane et Ieke Moerdijk. Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Springer-Verlag, 1992.
- Bart Jacobs. Categorical Logic and Type Theory. Elsevier, 1999.
à part le 1 du premier.

André Joyal and Ross Street. Braided tensor categories, Advances in Mathematics 102 (1993), 20?78. Pas disponible sur le web, photocopier à la bibliothèque.

F. William Lawvere. Taking categories seriously. Originally published as: Revista Colombiana de Matematicas, XX (1986) 147-178. Republished in: Reprints in Theory and Applications of Categories, No. 8 (2005) pp. 1-24
Fanny Dufosse.

John C. Baez and Aaron D. Lauda. Higher-dimensional algebra V: 2-Groups. Theory and Applications of Categories, Vol. 12, 2004, No. 14, pp 423-491.
Romain Demangeon.

Catégories pour l'informatique

Yves Guiraud. The three dimensions of proofs. Annals of Pure and Applied Logic 141(1-2):266-295 (2006).
Thibaut Balabonski.

Paul Taylor. Sober Spaces and Continuations. Theory and Applications of Categories 10 (2002) 248-299.
Jérémy Planul.

Jiri Adamek. Introduction to coalgebra. Theory and Applications of Categories, Vol. 14, 2005, No. 8, pp 157-199.
Ivan Morel.

Paul Blain Levy. Adjunction models for call-by-push-value with stacks. Theory and Applications of Categories, Vol. 14, 2005, No. 5, pp 75-110.
Michal Palka.

Robin Milner and Ole Høgh Jensen. Bigraphs and mobile processes (revised). Technical Report TR580, University of Cambridge Computer Laboratory, 2004.
Thomas Braibant.

T. Altenkirch, P. Dybjer, M. Hofmann, and P. Scott. Normalization by evaluation for typed lambda calculus with coproducts. 16th Symposium on Logic in Computer Science (LICS), 2001.
Martin Delacourt.

T. Altenkirch and B. Reus. Monadic presentations of lambda terms using generalized inductive types. Computer Science Logic (CSL), 1999.
Guillaume Munch.

T. Altenkirch, M. Hofmann, and T.Streicher. Categorical reconstruction of a reduction free normalization proof. Category Theory and Computer Science (CTCS), 1995.
Florian Hatat.

M. Hofmann. On the interpretation of type theory in locally cartesian closed categories. Proc. CSL '94, Kazimierz, Poland. Jerzy Tiuryn and Leszek Pacholski, eds. Springer LNCS, Vol. 933.

P. Selinger. Control categories and duality: on the categorical semantics of the lambda-mu calculus. Mathematical Structures in Computer Science 11:207-260, 2001. A lire impérativement avec Some remarks on control categories.

M. Hasegawa. Categorical glueing and logical predicates for models of linear logic. Preprint RIMS-1223, Kyoto University, January 1999.

C. Hermida. Fibrations, Logical Predicates and Indeterminates, Ph.D. thesis, ECS-LFCS-93277, University of Edinburgh, 1993.
Pierre Rannou.

V. Pratt. Chu Spaces avec un de ces papiers introductifs (en section 1).
Laurent Boyer.

N. Benton et M. Hyland. Traced Premonoidal Categories. Theoretical Informatics and Applications 37(4):273-299, © EDP Sciences 2003. pdf.
Sylvain Collange.

Trucs plus traditionnels

T. Altenkirch and C. McBride. Towards Observational Type Theory.

N. Benton. A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models. Proceedings of Computer Science Logic '94, Kazimierz, Poland. Springer-Verlag LNCS 933. June 1995. [15 page version] © Springer-Verlag 1995.

Y. Lafont, Interaction Combinators, Information and Computation 137 (1), p. 69-101, Academic Press (1997). (PS.GZ).
Bertrand Marc.

C. B. Jay and N. Ghani. The Virtues of Eta-Expansion. Journal of Functional Programming, vol. 15, no. 2, 1995. (PS).
Jonatan Lindén.

René Vestergaard. Primitive and Some/Any Proof Principles for beta-Standardisation. Preliminary version (the proof of Lemma 19 contains an error (in Figure 10), as it stands). (PDF).

Kanovitch, M. (1992). Horn-programming in linear logic is NP-complete. In Proceedings of the 7th Annual IEEE Symposium on Logic in Computer Science, pp. 200-210. (A la bibliothèque).

P. Baillot and Terui, K., Light types for polynomial time computation in lambda-calculus, Proceedings of LICS 2004, pp. 266--275 (2004).(PS).

Proof nets and explicit substitutions. Roberto Di Cosmo, Delia Kesner & Emmanuel Polonovski. Mathematical Structures in Computer Science, Volume 13, number 3, p. 409-450, 2003. (PS).

M. Hasegawa, Classical linear logic of implications. Mathematical Structures in Computer Science 15(2):323-342, April 2005. (PS.GZ).

M. Hasegawa, Girard translation and logical predicates. Journal of Functional Programming 10(1): 77-89, January 2000. (PS.GZ).

P.-L. Curien et Hugo Herbelin. The duality of computation. In Proceedings of the International Conference on Functional Programming, 2000. (PS.GZ).

P. Wadler. Call-by-value is dual to call-by-name. Proceedings of the International Conference on Functional Programming, 2003. (PDF).
Anne-Cécile Orgerie.

T. Ehrhard, L. Regnier. Differential interaction nets. Theoretical Computer Science, Elsevier, 2006. To appear. pdf.

G. Dowek, Lambda-calculus, combinators and the comprehension scheme, M. Dezani-Ciancaglini and G. Plotkin (Eds.), Typed Lambda Calculi and Applications, Lecture Notes in Computer Science 902, Springer-Verlag, 1995, pp. 154-170. Rapport de Recherche 2565, INRIA, 1995. (PS.GZ).

R. Hindley and G. Longo. Lambda-calculus models and extensionality. Z. Math. Logik Grundlag. Math., 26(4):289-310, 1980. (Pas disponible sur le web, passer à mon bureau pour le photocopier.)

J. B. Wells. Typability and type checking in System F are equivalent and undecidable. Ann. Pure Appl. Logic, 98(1-3):111-156, 1999. (PS).
Etienne Miret.

A. J. Kfoury and J. B. Wells. New notions of reduction and non-semantic proofs of beta -strong normalization in typed lambda -calculi. In Proc. 10th Ann. IEEE Symp. Logic in Comput. Sci., pages 311-321, 1995. (PS).

Gordon Plotkin. Call-by-Name, Call-by Value and the Lambda Calculus Reproduced from Theoretical Computer Science, Vol. 1, pp. 125-159, Copyright (1975), with permission from Elsevier. (PS).
Denis Kuperberg.

A. Miquel. Lambda-Z: Zermelo's Set Theory as a PTS with 4 Sorts. In Types for Proofs and Programs (TYPES'04). Résumé. (Passer l'imprimer à mon bureau.)

O. Laurent. Polarized proof-nets and lambda-mu calculus. Theoretical Computer Science, 290(1):161-188. Janvier 2003. (PS.GZ).