Lionel Vaux Auclair

Publications acceptées

Journaux

Finitary Simulation of Infinitary β-Reduction via Taylor Expansion, and Applications: (with Rémy Cerda); Logical Methods in Computer Science, Volume 19, Issue 2 (December 20, 2023); Last modified: 2023-12-19.
On the Taylor expansion of λ-terms and the groupoid structure of their rigid approximants: (with Federico Olimpieri); Journal version of our contribution to TLLA 2018.; Logical Methods in Computer Science, Volume 18, Issue 1 (January 6, 2022)
An application of parallel cut elimination in multiplicative linear logic to the Taylor expansion of proof nets: (with Jules Chouquet); Much expanded rewriting of our contribution to CSL 2018, including a treatment of full MELL, with weakening.; Logical Methods in Computer Science, Volume 17, Issue 4 (December 20, 2021)
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. This includes full proofs as well as a detailed analysis of parallel resource reduction and the generalization of non-deterministic Böhm trees.; Logical Methods in Computer Science, Volume 15, Issue 3 (July 31, 2019).; Last modified: 2018-02-16.
Transport of finiteness structures and applications: (with Christine Tasson); Mathematical Structures in Computer Science, Volume 28, Issue 7, 2018, pp. 1061--1096, 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. Fixing the proof requires new techniques that we developped with Axel Kerinec: these were presented at the Scalp 2019 meeting, and then more formally at the HOR 2023 workshop.; 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

Strategies as Resource Terms, and their Categorical Semantics: (with Lison Blondeau-Patissier and Pierre Clairambault); Proceedings of FSCD 2023.
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.
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

The algebraic λ-calculus is a conservative extension of the ordinary λ-calculus: (with Axel Kerinec); Presented at the 11th International Workshop on Higher-Order Rewriting, Rome, Italy 4 July 2023; Slides of my HOR 2023 talk.; Last modified: 2023-06-15.
How To Play The Accordion. On the (Non-)Conservativity of the Reduction Induced by the Taylor Approximation of λ-Terms: (with Rémy Cerda); Presented at the 7th International Workshop on Trends in Linear Logic and Applications; Last modified: 2023-06-16.
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

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.

The algebraic λ-calculus, 12 years later: a conservativity proof at last (proof that the equivalence induced on λ-terms by the reduction of algebraic λ-terms is the same as β-reduction): (with Axel Kerinec); Slides of my talk at the Scalp 2019 meeting in Lyon, 17-18 October 2019.
(∀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

Cours de Calculabilité pour le DIU EIL dans l’académie d’Aix-Marseille, en 2019.: L’archive contient les fichiers sources, placées sous licence CC-BY-SA.
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é.; J’ai présenté une nouvelle version révisée de cet exposé à la fête de la science au lycée Val de Durance de Pertuis, le 10 octobre 2019.; 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.

Publications

Sur cette page:

Juste à côté: