Lionel Vaux

Publications acceptées

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

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.

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.

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.

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.

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.

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.

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.