Publications acceptées
Journaux
- Normalizing the Taylor expansion of non-deterministic λ-terms, via parallel reduction of resource vectors
-
Very much expanded version of the CSL 2017 paper Taylor expansion, β-reduction and normalization (see below).
This includes full proofs as well as a detailed analysis of parallel resource reduction
and the generalization of non-deterministic Böhm trees.
- To appear in Logical Methods in Computer Science (selected paper of CSL 2017).
- Last modified: 2018-02-16.
- Transport of finiteness structures and applications
- (with Christine Tasson)
- Mathematical Structures in Computer Science, Volume 15, Issue 4, August 2005, pp. 615-646,
DOI:10.1017/S0960129516000384.
- Last modified: 2016-12-14.
- A non-uniform finitary relational semantics of system T
- RAIRO - Theoretical Informatics and Applications, 47, pp 111-132,
January 2013, DOI:10.1051/ita/2012031.
- Extended and updated version of the FICS 2009 paper.
- Last modified: 2011-11-21.
- The algebraic lambda-calculus
- Mathematical Structures in Computer Science,
Volume 19, issue 05, pp. 1029-1059, October 2009,
DOI:10.1017/S0960129509990089.
- Erratum: there is a serious mistake in the proof of conservativity,
and I have no clue how to fix it in general. Conservativity can be proved
for normalisable terms, following the same left-reduction technique as for
Taylor expansion [arxiv:1706.04700].
To my knowledge, the general case is still open.
- Last modified: 2009-05-23.
- The differential lambda-mu-calculus
- Theoretical Computer Science,
Volume 379, Issues 1-2, 12 June 2007, Pages 166-209,
DOI:10.1016/j.tcs.2007.02.028.
- Last modified: 2006-12-06.
Conférences internationales
- An application of parallel cut elimination in unit-free multiplicative
linear logic to the Taylor expansion of proof nets
- (with Jules Chouquet)
- Proceedings of CSL 2018.
- Last modified: 2018-05-29.
- Taylor expansion, β-reduction and normalization
- Proceedings of CSL 2017, LIPIcs Volume 82.
DOI:10.4230/LIPIcs.CSL.2017.39.
- Slides of my CSL 2017 talk (slightly fixed).
- Last modified: 2017-06-26.
- Strong Normalizability as a Finiteness Structure via the Taylor Expansion of λ-terms
- (with Michele Pagani
and Christine Tasson).
- Proceedings of FoSSaCS 2016, LNCS Volume 9634, 2016.
DOI:10.1007/978-3-662-49630-5_24.
- Slides of my FoSSaCS 2016 talk.
- Last modified: 2016-01-08.
- Differential linear logic and polarization
- Proceedings of TLCA 2009,
LNCS Volume 5608, 2009.
DOI:10.1007/978-3-642-02273-9_27.
- Slides of my TLCA09 talk (the speaker was Michele
Pagani).
- Last modified: 2009-05-06.
- On linear combinations of lambda-terms
- Proceedings of RTA 2007,
LNCS Volume 4533, June 2007.
DOI:10.1007/978-3-540-73449-9_28.
- Best paper award of RTA 2007.
- Slides of my RTA 2007 talk.
- Last modified: 2007-02-03.
- Convolution lambda-bar-mu-calculus
- Proceedings of TLCA 2007,
LNCS Volume 4583, June 2007.
DOI:10.1007/978-3-540-73228-0_27.
- Errata.
- Slides of my TLCA07 talk.
- Last modified: 2007-05-30.
Workshops internationaux
- On the Taylor expansion of λ-terms and the groupoid
structure of their rigid approximants
- (with Federico Olimpieri)
- Joint Workshop on Linearity & TLLA, Oxford, 7–8 July, 2018.
- Last modified: 2018-04-30.
- Normalization by Evaluation in Linear Logic
- (with Jules Chouquet, Giulio Guerrieri and Luc Pellissier)
- International Workshop on Trends in Linear Logic and Applications (TLLA), Oxford, September 3, 2017.
- Last modified: 2017-06-19.
- On the transport of finiteness structures
- 5th International Conference on Topology, Algebra and
Categories in Logic, TACL 2011.
- Slides of my talk.
- Last modified: 2011-06-18.
- A non-uniform finitary relational semantics of system T
- 6th Workshop on Fixed Points in Computer Science, FICS 2009.
- Slides of my FICS09 talk.
- Last modified: 2009-08-11.
Chapitres de livres
- Programmes, preuves et fonctions : le
ménage à trois de Curry-Howard
- (avec Emmanuel Beffara)
- Chapitre du livre: Informatique
Mathématique: une photographie en 2013, Philippe Langlois
éd., publié aux PUP, 2013
- Diapositives de nos
exposés.
Notes et prépublications
- Primitive recursion in finiteness spaces
- Research report, Laboratoire de Mathématiques de
l'Université de Savoie, 2009.
- Last modified: 2009-05-11.
- Lambda-calculus in an algebraic setting
- Research report, Institut de Mathématiques de Luminy, 2006.
- Last modified: 2006-04-21.
- A type system with implicit types
- Note, École Normale Supérieure de Lyon, 2004.
- A note on an implicit calculus with annotated terms:
introducing universal dependent types
- Note, École Normale Supérieure de Lyon, 2004.
Communications
On retrouve ci-dessous des supports d’exposés et des documents qui
n’étaient pas associés à des publications.
- (∀M∈Λ₊) M∈SN ⟺ T(M)∈F
(A characterization of strong normalizability by a finiteness structure via the Taylor expansion of λ-terms)
- (with Michele Pagani and Christine Tasson)
- Slides of my talk at the Geocal-LAC-LTP 2015 meeting in Nancy, 12-14 Oct. 2015.
- From linearity in
coherence spaces to Linear Logic
- Slides of my lecture at the logic school on Linear
Logic, Ludics and Geometry of Interaction in Paraty
(Brazil), 27 Aug. to 1st Sep. 2012.
- An introduction to
ludics
- Slides of a tutorial talk for the symposium
Rebuilding Logic and Rethinking Language in Interaction
terms,
affiliated to the 14th
CLMPS in Nancy, July 2011.
- Introduction à (une
introduction à) la ludique
- Notes d'exposé, rencontre du projet ANR LOCI, 20 et 21
janvier 2011, CIRM.
- Last modified: 2011-01-20.
Enseignement et diffusion de la culture scientifique
- L’informatique, c’est pas l’automatique
- Support de mon exposé au forum des mathématiques de Marseille 2013,
les 4 et 5 avril à l’École de la Deuxième Chance.
- Complément : le fichier source
d’un exemple de programme
qui tourne de manière identique sous Linux, Windows, Android, etc.
- Une version
révisée de cet exposé a été donnée au 4ème forum des
mathématiques en pays d’Aix en janvier 2015. Les élèves du
lycée Pasquet ont gagné le concours du forum
en rédigeant une
présentation de cet exposé.
- Ces transparents (ou une variante) me servent
régulièrement pour animer un atelier grand public
intitulé L’informatique derrière les clics
(titre volé à Guillaume Theyssier):
on y alterne des considérations sur
l’universalité des notions de codage et de calcul,
et des manipulations directes de matériel et de logiciel
informatique.
- Recherche en mathématiques pour les élèves de lycée: l'exemple des stages Hippocampe
- (avec Pierre Arnoux)
- Actes du Colloque Espace Mathématique Francophone 2012, G.T. 10 :
La démarche d’investigation dans la classe de
mathématiques: fondements et pratiques.
Université de Genève, 3-7 février 2012.
Rapports de stage
Quand j'étais petit, j'étais élève de l'ÉNS de Lyon. J'ai
effectué trois stages après lesquels j'ai rédigé les rapports suivants:
- Étude du λ-calcul
différentiel et extension au cas classique: le
λμ-calcul différentiel.
- Sous la direction de Thomas Ehrhard et Laurent Regnier,
Institut de Mathématiques de Luminy, Marseille.
- Stage de DEA d'Informatique Fondamentale, ÉNS
Lyon/Université Lyon 1, 2004.
- Un calcul des constructions
implicite.
- Sous la direction de Thierry Coquand,
Göteborgs universitet, Suède.
- Stage de Maîtrise d'Informatique, ÉNS
Lyon/Université Lyon 1, 2003.
- Flots circulaires.
- Sous la direction d'André Raspaud,
LaBRI, Bordeaux.
- Stage de Licence d'Informatique, ÉNS
Lyon/Université Lyon 1, 2002.
