Master Parisien de Recherche en Informatique
Lambda-calculs et catégories
Cours M1.20
Cours Magistral
Lecture one : general presentation, categories and functors, cartesian categories
Lecture two : natural transformations, the 2-category of categories, string diagrams
Lecture four : finite developments, algebraic Church-Rosser theorem, event structures, asynchronous graphs
Lecture five : simply-typed lambda-calculus, cartesian closed categories, lambda-calculus with computational effects
Lecture six : limits and colimits, Kan extensions, monoids and mnemoids, semantics of local states, presheaf categories
Travaux Dirigés
Références bibliographiques du cours
Quelques pointeurs utiles sur la théorie des catégories
If you want to know more on the unifying role of category theory in various fields
of mathematics and computer science, you are welcome to visit this dedicated blog:
If you are interested in the recent connection between homotopy theory and type theory,
a natural place to have a look at is this website:
You may also have a look at these books.
-
John Baez. Lectures on n-categories and cohomology.
[fichier pdf]
-
Audun Holme. Basic Modern Algebraic Geometry -- Introduction to Grothendieck's Theory of Schemes.
[fichier pdf]
-
Peter May. A concise course in algebraic topology.
[fichier pdf]
Articles et pointeurs
A selection (always in development) of papers and surveys on the topic:
-
Samson Abramsky, Guy McCusker: game semantics.
[fichier pdf]
-
Samson Abramsky, Guy McCusker: linearity, sharing and state: a fully abstract game semantics for Idealized Algol with active expressions.
[fichier pdf]
-
R. D. Arthan: a traced monoidal category of relations.
[fichier pdf]
-
Patrick Cousot: types as abstract interpretations.
[fichier pdf]
-
Pierre-Louis Curien: substitutions up to isomorphisms.
[fichier pdf]
-
Pierre-Louis Curien: category theory, a programming-language introduction.
[fichier pdf]
-
Olivier Danvy, Jürgen Koslowski, Karoline Malmkjær: compiling monads.
[fichier pdf]
-
Marcelo Fiore, Nicola Gambino, Martin Hyland, Glynn Winskel:
[fichier pdf]
-
Daniel P. Friedman: from direct style to monadic style through
continuation passing style.
[fichier pdf]
-
Daniel P. Friedman: direct style from monadic style and back.
[fichier pdf]
-
Greg Friedman: an elementary illustrated introduction to simplicial sets.
[fichier pdf]
-
Carsten Fuhrmann: direct models of the computational lambda-calculus.
[fichier pdf]
-
Nicola Gambino, Martin Hyland: well-founded trees and dependent polynomial functors.
[fichier pdf]
-
Richard Garner: two-dimensional models of type theory.
[fichier pdf]
-
Dan Ghica: geometry of synthesis.
[fichier pdf]
-
Thérèse Hardin, Luc Maranget, Bruno Pagano:
functional runtime systems within the lambda-sigma calculus.
[fichier pdf]
-
Russ Harmer, Martin Hyland, Paul-André Melliès:
categorical combinatorics for innocent strategies.
[fichier pdf]
-
Barnaby Hilken: towards a proof-theory of rewriting: the simply-typed
2-lambda-calculus.
[fichier pdf]
-
Peter Hines, Philip Scott: conditional quantum iteration from categorical traces.
[fichier pdf]
-
Martin Hofmann:
Syntax and Semantics of Dependent Types
[fichier pdf]
-
Martin Hyland: the effective topos.
[fichier pdf]
-
Martin Hyland and John Power: the category theoretic understanding of universal algebra: Lawvere theories and monads.
[fichier pdf]
-
Martin Hyland, Paul Blain Levy, Gordon Plotkin, John Power:
combining algebraic effects with continuations.
[fichier pdf]
-
André Joyal. Une théorie combinatoire des séries formelles.
Advances in Mathematics, 42(1) :1 1981.
-
André Joyal, Ross Street, Dominic Verity: traced monoidal categories.
[fichier pdf]
-
Joachim Kock: notes on polynomial functors.
[fichier pdf]
-
Jean-Louis Krivine: Typed lambda-calculus in classical Zermelo-Fraenkel set theory.
[fichier pdf]
-
Yves Lafont, Alain Prouté:
Church-Rosser property and homology of monoids.
[fichier pdf]
-
Paul-André Melliès: functorial boxes in string diagrams.
[fichier pdf]
-
Paul-André Melliès: the true concurrency of innocence.
[fichier pdf]
-
Eugenio Moggi: computational lambda-calculus and monads.
[fichier pdf]
-
Luke Ong: on model-checking trees generated by higher-order recursion schemes.
[fichier pdf]
-
Andy Pitts: polymorphism is set-theoretic, constructively.
[fichier pdf]
-
Gordon Plotkin, John Power: computational effects determine monads.
[fichier pdf]
[erratum]
-
RAG Seely:
categorical semantics for higher order polymorphic lambda calculus.
[fichier pdf]
-
RAG Seely:
modeling computations: a 2-categorical framework.
[fichier pdf]
-
Peter Selinger:
Control categories and duality: on the categorical semantics of the lambda-mu calculus.
[fichier pdf]
-
Julianna Szido: le lambda-calcul vu comme monade initiale.
[fichier pdf]
-
Glynn Winskel, Mogens Nielsen: models for concurrency.
[fichier pdf]
Calendrier des soutenances de cette année
Lundi 12 janvier 2015 :
Salle R le matin, Salle S16 l'après-midi
9h -- 9h30 Adrien Husson
Patrick Cousot: types as abstract interpretations.
9h30 -- 10h Jonathan Laurent
Roland Backhouse, Patrick Jansson, Johan Jeurig, Lambert Meertens: Generic Programming.
10h -- 10h30 Alex Auvolat
Olivier Danvy, Jurgen Koslowski, Karoline Malmkjaer: Compiling monads.
10h30 -- 11h Pause
11h -- 11h30 Thomas Espitau
Tracing Man-in-th-Middle in Monoidal categories.
11h30 -- 12h Maxime Chaminadour
Dwyer et Spalinski: Homotopy theories and model categories.
Attention: soutenances en Salle S16 l'après-midi
14h -- 14h30 Diane Gallois-Wong
Joachim Kock: notes on polynomial functors.
14h30 -- 15h Raphaël Rieu-Helft
Eugenio Moggi: Computational lambda-calculus and monads
Vendredi 16 janvier 2015 en salle S16
14h -- 14h30 Marc de Visme:
Dan Ghica: Geometry of Synthesis.
14h30 -- 15h Théo Winterhalter:
Gordon Plotkin, John Power: computational effects determine monads.
15h -- 15h30 Mathias Sablé Meyer:
Martin Hyland, Paul Blain Levy, Gordon Plotkin, John Power: combining algebraic effects with continuations.
15h30 -- 16h Pause
16h -- 16h30 François Thiré:
Philip Wadler: Monads for functional programming
16h30 -- 17h Victor Lanvin
Martin Hyland, Paul Blain Levy, Gordon Plotkin, John Power: combining algebraic effects with continuations.
17h -- 17h30 Thomas Magnard
Pierre-Louis Curien: substitutions up to isomorphisms
17h30 -- 18h Amir-hossein Bateni
Dimitri Kartsaklis et Mehrnoosh Sadrzadeh: A Study of Entanglement in a Categorical Framework of Natural Language.
18h -- 18h30 Olivier Marty
Olivier Danvy, Jürgen Koslowski, Karoline Malmkjær: Compiling monads.
18h30 -- 19h Elie Michel
Phil Wadler: theorems for free!
Lundi 19 janvier 2015 : salle R le matin, salle INF 1 l'après-midi
9h -- 9h30 Nicolas Jeannerod
Jean-Louis Krivine: Typed lambda-calculus in classical Zermelo-Fraenkel set theory.
9h30 -- 10h Mathieu Lehaut
Gordon Plotkin et John Power: Computational effects determine monads.
10h -- 10h30 Remi Bricout
Samson Abramsky et Guy McCusker: Game semantics
10h30 -- 11h Pause
11h -- 11h30 Félicien Comtat
Martin Hyland: the effective topos.
11h -- 11h30 Theo Karaboghossian
André Joyal: une théorie combinatoire des séries formelles.
12h -- 12h30 Pierre Ludmann
Martin Hyland and John Power: the category theoretic understanding of universal algebra: Lawvere theories and monads
12h30 -- 13h Maxime Legrand
Samson Abramsky, Guy McCusker: game semantics
13h -- 14h Pause
Attention: soutenances en Salle INF 1 l'après-midi
14h -- 14h30 Pierre-Léo Bégay
Martin Hofmann: Syntax and Semantics of Dependent Types.
14h30 -- 15h Ikram Cherigui
Andy Pitts: polymorphism is set-theoretic, constructively.
15h -- 15h30 Louis Hauseux
André Joyal: Une théorie combinatoire des séries formelles.
15h30 -- 16h Pause
16h -- 16h30 Itsaka Rakotonirina
Thérèse Hardin, Luc Maranget, Bruno Pagano:
functional runtime systems within the lambda-sigma calculus.
16h30 -- 17h Leo Tible
17h -- 17h30 Christophe Cordero
André Joyal. Une théorie combinatoire des séries formelles.
17h30 -- 18h Paul Gallot
Joyal, Street, Verity: Traced monoidal categories
Quelques liens utiles