Publications

Book chapters

Journals

• J. Espírito Santo and D. Kesner and L. Peyrot. A Faithful and Quantitative Notion of Distant Reduction for the Lambda-Calculus with Generalized Applications.
  Logical Methods in Computer Science (LMCS), to appear.

• E. Bonelli and D. Kesner and A. Viso. A Strong Bisimulation for a Classical Term Calculus.
  Logical Methods in Computer Science (LMCS), to appear.

• D. Kesner and L. Peyrot and D. Ventura. Node Replication: Theory and Practice.
  Logical Methods in Computer Science (LMCS), 20(1):1--66, 2024.

• A. Bucciarelli and D. Kesner and A. Ríos and A. Viso. The Bang Calculus Revisited.
  Information and Computation (I&C), 293:105047, 2023.

• V. Arrial and D. Kesner and G. Guerrieri. Quantitative Inhabitation for Different Lambda Calculi in a Unifying Framework.
  Proc. of the ACM on Programming Languages Journal (PACMPL), 7(POPL), 2023.
  

• D. Kesner. A Fine-Grained Computational Interpretation of Girard's Intuitionistic Proof-Nets.
  Proc. of the ACM on Programming Languages Journal (PACMPL), 6(POPL):8:1--8:28, 2022.
  

• A. Bucciarelli and D. Kesner and S. Ronchi Della Rocca. Solvability=Typability+Inhabitation.
  Logical Methods in Computer Science (LMCS), 17(1):1--27, 2021.
  

• B. Accattoli and S. Graham-Lengrand and D. Kesner. Tight Typings and Split Bounds, Fully Developed.
  Journal of Functional Programming (JFP), 30(14):1--85, 2020.
  

• D. Kesner and P. Vial. Non-idempotent types for classical calculi in natural deduction style.
  Logical Methods in Computer Science (LMCS), 16(1):1--46, 2020.

• D. Kesner and D. Ventura. A resource aware semantics for a focused intuitionistic calculus.
  Mathematical Structures in Computer Science (MSCS), 29(1):93--126, 2019 (published online 22 May 2017).
  

• B. Accattoli and S. Graham-Lengrand and D. Kesner. Tight Typings and Split Bounds.
  Proc. of the ACM on Programming Languages Journal (PACMPL), 2(ICFP):94:1--94:30, 2018.
  

• A. Bucciarelli and D. Kesner and S. Ronchi Della Rocca. Inhabitation for Intersection Types.
  Logical Methods in Computer Science (LMCS), 14(3):1--28, 2018.

• T. Balabonski and E. Bonelli and P. Barenbaum and D. Kesner. Foundations of Strong Call by Need.
  Proc. of the ACM on Programming Languages Journal (PACMPL), 1(1):20:1--20:29, 2017.
  

• A. Bucciarelli and D. Kesner and D. Ventura. Non-Idempotent Intersection Types for the Lambda-Calculus.
  Logic Journal of the IGPL, 25(4):431--464, 2017.
  

• E. Bonelli and D. Kesner and C. Lombardi and A. Ríos. On abstract normalisation beyond neededness.
  Theoretical Computer Science (TCS), 672:36--63, 2017.
  

• B. Accattoli and D. Kesner. Preservation of strong normalisation modulo permutations for the structural calculus.
  Logical Methods in Computer Science (LMCS), 8(1):1--44, 2012.
  

• D. Kesner and F. Renaud. A prismoid framework for languages with resources.
  Theoretical Computer Science (TCS), 412(37):4867--4892, 2011.

• D. Kesner. A Theory of Explicit Substitutions with Safe and Full Composition.
  Logical Methods in Computer Science (LMCS), 5(3):1--29, 2009.

• B. Jay and D. Kesner. First-class patterns.
  Journal of Functional Programming (JFP), 19(2): 191--225, 2009.

• J. Forest and D. Kesner. Expression Reduction Systems with Patterns.
  Journal of Automated Reasoning (JAR), 39(4):513--541, 2007.

• D. Kesner and S. Lengrand. Resource Operators for lambda-calculus.
  Information and Computation (I&C), 205(4):419--473, 2007.

• E. Bonelli and D. Kesner and A. Ríos. de Bruijn Indices for MetaTerms.
  Journal of Logic and Computation (JLC), 15(6): 855--899, 2005.
  

• E. Bonelli and D. Kesner and A. Ríos. Relating Higher-Order and First-Order Rewriting.
  Journal of Logic and Computation (JLC), 15(6): 901--947, 2005.

• S. Cerrito and D. Kesner. Pattern Matching as Cut Elimination.
  Theoretical Computer Science (TCS), 323(1-3):71--127, 2004.

• R. Di Cosmo and D. Kesner and E. Polonovski. Proof Nets and Explicit Substitutions.
  Mathematical Structures in Computer Science (MSCS), 13(3): 409--450, 2003.

• D. Kesner. Confluence of Extensional and Non-Extensional lambda-calculi with Explicit Substitutions.
  Theoretical Computer Science (TCS), 238(1-2): 183--220, 2000.

• D. Kesner and P. E. Martínez López. Explicit Substitutions for Objects and Functions.
  Journal of Functional and Logic Programming (JFLP), Special Issue 2:1--33, Vol 1999.

• M. Ferreira and D. Kesner and L. Puel. Lambda-calculi with Explicit Substitutions Preserving Strong Normalization.
  Applicable Algebra in Engineering, Communication and Computing (AAECC), 9(4): 333--371, 1999.

• D. Kesner. Reasoning about redundant patterns.
  Journal of Functional and Logic Programming (JLFP), Number 4:3--48, Vol 1997.

• R. Di Cosmo and D. Kesner. Combining algebraic rewriting systems, extensional lambda-calculi and fixpoints.
  Theoretical Computer Science (TCS), 169(2): 201--220, 1996.

• D. Kesner and L. Puel and V. Tannen. A typed pattern calculus.
  Information and Computation (I&C), 124(1):32--61, 1995.

• R. Di Cosmo and D. Kesner. Simulating expansions without expansions.
  Mathematical Structures in Computer Science (MSCS), 4(3): 315--362, 1994.

Conferences

• P. Barenbaum and D. Kesner and M. Milicich. Hybrid Intersection Types for PCF.
  Proc. of the 25th Int. Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR).
  EPiC Series in Computing, Mauritius, May 2024, to appear.
  (pdf)

• V. Arrial and D. Kesner and G. Guerrieri. The Benefits of Diligence.
  Proc. of the International Joint Conference on Automated Reasoning (IJCAR).
  LNAI, Nancy, France, July 2024, to appear.
  (pdf)

• S. Alves and D. Kesner and M. Ramos. Quantitative Global Memory.
  29th Workshop on Logic, Language, Information and Computation (WoLLIC).
  LNCS 13923, pages 53--68, Halifax, Canada, July 2023.
  (pdf)

• D. Kesner and L. Peyrot. Solvability for Generalized Applications.
  Proc. of the 7th International Conference on Formal Structures for Computation and Deduction (FSCD).
  LIPIcs, Vol 228 , pages 18:1--18:22, Haifa, Israel, August 2022.
  (pdf)

• J. Espírito Santo and D. Kesner and L. Peyrot. A Faithful and Quantitative Notion of Distant Reduction for Generalized Applications.
  Proc. of the 24th Int. Conference on Foundations of Software Science and Computation Structures (FoSSaCS).
  LNCS 13242, Munich, Germany, April 2022.
  (pdf)

• D. Kesner and A. Viso. Encoding Tight Typing in a Unified Framework.
  Proc. of the 29th EACSL International Conference on Computer Science and Logic (CSL).
  LIPIcs, Vol 216 , pages 25:1--25:20, Göttingen, Germany, January 2022.
  (pdf)

• D. Kesner and L. Peyrot and D. Ventura. The Spirit of Node Replication.
  Proc. of the 23rd Int. Conference on Foundations of Software Science and Computation S tructures (FoSSaCS).
  LNCS 12650, pages 344--364, Luxembourg, Luxembourg, March-April 2021.
  (pdf)

• D. Kesner and P. Vial. Consuming and Persistent Types for Classical Logic.
  Proc. of the 35th of the ACM/IEEE Symposium on Logic in Computer Science (LICS).
  ACM, pages 619--632, Saarbrucken, Germany, July 2020.
  (pdf)

• A. Bucciarelli and D. Kesner and A. Ríos and A. Viso. The Bang Calculus Revisited.
  Proc. of the 15th International Symposium on Functional and Logic Programming (FLOPS).
  LNCS 12073, pages 13--32, Akito, Japan, April 2020.
  (pdf)

• D. Kesner and E. Bonelli and A. Viso. Strong Bisimulation for Control Operators (Invited Paper).
  Proc. of the 28th EACSL International Conference on Computer Science and Logic (CSL).
  LIPIcs, Vol 152, pages 4:1--4:23, Barcelona, Spain, January 2020.
  (pdf)

• S. Alves and D. Kesner and D. Ventura. A Quantitative Understanding of Pattern Matching.
  Post-Proc of the 25th International Conference on Types for Proofs and Programs (TYPES).
  LIPIcs, Vol 175, pages 3:1--3:36, Oslo, Norway, June 2019.
  (pdf)

• D. Kesner and A. Ríos and A. Viso. Call-by-need, neededness and all that.
  Proc. of the 20th Int. Conference on Foundations of Software Science and Computation Structures (FoSSaCS).
  LNCS 10803, pages 241--257, Thessaloniki, Greece, April 2018.
  (pdf)

• D. Kesner and P. Vial. Types as Resources for Classical Natural Deduction.
  Proc. of the Second International Conference on Formal Structures for Computation and Deduction (FSCD).
  LIPIcs, Vol 84, pages 24:1--24:17, Oxford, UK, September 2017.
  (pdf)

• D. Kesner. Reasoning about call-by-need by means of types.
  Proc. of the 19th Int. Conference on Foundations of Software Science and Computation Structures (FoSSaCS).
  LNCS 9634, pages 424-441, Eindhoven, The Netherlands, April 2016.
  (pdf)

• A. Bucciarelli and D. Kesner and D. Ventura. Strong Normalization through Intersection Types and Memory.
  Proc. of the 10th Int. Workshop on Logical and Semantical Frameworks, with Applications (LSFA).
  ENTCS, Vol 323, pages 75--91, 2016.
  (pdf)

• D. Kesner and D. Ventura. A resource aware computational interpretation for Herberlin's syntax.
  Proc. of the 12th Int. Colloquium on Theoretical Aspects of Computing (ICTAC).
  LNCS 9399, pages 1--16, Cali, Colombia, September 2015.
  (pdf)

• A. Bucciarelli and D. Kesner and S. Ronchi Della Rocca. Observability for Pair Pattern Calculi.
  Proc. of the 13th Int. Conference on Typed Lambda Calculi and Applications (TLCA).
  LIPIcs, Vol 38, pages 123--137, Warsaw, Poland, July 2015.
  (pdf)

• F. L. C. de Moura and D. Kesner and M. Ayala-Rincón . Metaconfluence of Calculi with Explicit Substitutions at a Distance.
  IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS).
  LIPIcs, Vol 29, pages 391--402, New Delhi, India, December 2014.
  (pdf)

• D. Kesner and D. Ventura. Quantitative Types for the Linear Substitution Calculus.
  Proc. of the 8th Int. Conference on Theoretical Computer Science (TCS).
  LNCS 8705, pages 296--310, Rome, Italy, September 2014.
  (pdf)

• A. Bucciarelli and D. Kesner and S. Ronchi Della Rocca. The Inhabitation Problem for Non-Idempotent Intersection Types.
  Proc. of the 8th Int. Conference on Theoretical Computer Science (TCS).
  LNCS 8705, pages 341--354 Rome, Italy, September 2014.
  (pdf)

• B. Accattoli and E. Bonelli and D. Kesner and C. Lombardi. A Nonstandard Standardization Theorem.
  Proc. of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL).
  ACM, pages 659--670, San Diego, USA, January 2014.
  (pdf)

• E. Bonelli and D. Kesner and C. Lombardi and A. Ríos. Normalisation for Dynamic Pattern Calculi.
  Proc. of the 23rd Int. Conference on Rewriting Techniques and Applications (RTA).
  LIPIcs, Vol 15, pages 117--132, Nagoya, Japan, May-June 2012.
  (pdf)

• B. Accattoli and D. Kesner. The permutative lambda-calculus.
  Proc. of the 18th Int. Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR).
  LNCS 7180, pages 23--36, Mérida, Venezuela, March 2012.
  (pdf)
  

• D. Kesner and C. Lombardi and A. Ríos. A Standardisation proof for algebraic pattern calculi.
  In the Proc. of 5th Int. Workshop on Higher-Order Rewriting (HOR 2010).
  EPTCS, Number 49, pages 58--72, Edinburgh, United Kingdom, July 2011.

• B. Accattoli and D. Kesner. The structural lambda-calculus.
  Proc. of the 19th EACSL International Conference on Computer Science and Logic (CSL).
  LNCS 6247, pages 381--395, Brno, Czech Republic, August 2010.
  (pdf) Technical Report

• D. Kesner and F. Renaud. The prismoid of resources.
  Proc. of the 34th Int. Symposium on Mathematical Foundations of Computer Science (MFCS).
  LNCS 5734, pages 464--476, Novy Smokovec, High Tatras, Slovakia, August 2009.
  (pdf)

• D. Kesner. Perpetuality for full and safe composition (in a constructive setting).
  Proc. of the 35th Int. Colloquium on Automata, Languages and Programming (ICALP), Part II.
  LNCS 5126, pages 311--322, Reykjavik, Iceland, July 2008.
  (pdf)

• D. Kesner. The Theory of Explicit Substitutions Revisited.
  Proc. of the 16th EACSL International Conference on Computer Science and Logic (CSL).
  LNCS 4646, pages 238--252, Lausanne, Switzerland, September 2007.
  (pdf)

• R. Dyckhoff and D. Kesner and S. Lengrand. Strong cut-elimination systems for Hudelmaier's depth-bounded sequent calculus for implicational logic.
  Proc. of the 3rd Int. Joint Conference on Automated Reasoning (IJCAR).
  LNAI 4130, pages 347--361, Seattle, USA, August 2006.
  (ps)

• B. Jay and D. Kesner. Pure pattern calculus.
  Proc. of the 15th European Symposium on Programming (ESOP).
  LNCS 3924, pages 100--114, Vienna, Austria, March-April 2006.
  (ps)

• D. Kesner and S. Lengrand. Extending the Explicit Substitution Paradigm.
  Proc. of the 16th Int. Conference on Rewriting Techniques and Applications (RTA).
  LNCS 3467, pages 407--422, Nara, Japan, April 2005.
  (ps)

• J. Forest and D. Kesner. Expression Reduction Systems with Patterns.
  Proc. of the 14th Int. Conference on Rewriting Techniques and Applications (RTA).
  LNCS 2706, pages 107--122, Valencia, Spain, June 2003.
  (ps)

• E. Bonelli and D. Kesner and A. Ríos. From Higher-Order to First-Order Rewriting.
  Proc. of the 12th Int. Conference on Rewriting Techniques and Applications (RTA).
  LNCS 2051, pages 47--62, Utrecht, The Netherlands, June 2001.
  (ps)

• E. Bonelli and D. Kesner and A. Ríos. A de Bruijn notation for higher-order rewriting.
  Proc. of the 11th Int. Conference on Rewriting Techniques and Applications (RTA).
  LNCS 1833, pages 62--79, Norwick, UK, July 2000.
  (ps)

• R. Di Cosmo and D. Kesner and E. Polonovski. Proof Nets and Explicit Substitutions.
  Proc. of the 3rd Int. Conference on Foundations of Software Science and Computation Structures (FoSSaCS).
  LNCS 1784, pages 63--81, Berlin, Germany, March/April, 2000.

• S. Cerrito and D. Kesner. Pattern Matching as Cut Elimination.
  Proc. of the 14th Annual IEEE Symposium on Logic in Computer Science (LICS).
  IEEE, pages 98--108, Trento, Italy, July 1999.
  (ps)

• D. Kesner and P. E. Martínez López. Explicit Substitutions for Objects and Functions.
  Proc. of the Joint Int. Symposiums
  Programming Languages, Implementations, Logics and Program (PLILP) and Algebraic and Logic Programming (ALP).
  LNCS 1490, pages 195--212, Pisa, Italy, September 1998.

• M. Ferreira and D. Kesner and L. Puel. Reducing AC-Termination to Termination.
  Proc. of the 23rd Int. Symposium on Mathematical Foundations of Computer Science (MFCS).
  LNCS 1450, pages 239--247, Brno, Czech Republic, August 1998.
  (ps)

• R. Di Cosmo and D. Kesner. Strong Normalization of Explicit Substitutions via Cut Elimination in Proof Nets.
  Proc. of the 12th Annual IEEE Symposium on Logic in Computer Science (LICS).
  IEEE, pages 35--45, Warsaw, Poland, July 1997.
  (ps)

• M. Ferreira and D. Kesner and L. Puel. Lambda-calculi with explicit substitutions and composition which preserve beta-strong normalization (Extended Abstract).
  Proc. of the 5th Int. Conference on Algebraic and Logic Programming (ALP).
  LNCS 1139, pages 284--298, Aachen, Germany, September 1996.
  (ps)

• D. Kesner. Confluence properties of extensional and non-extensional lambda-calculi with explicit substitutions.
  Proc. of the 7th Int. Conference on Rewriting Techniques and Applications (RTA).
  LNCS 1103, pages 184--199, New Brunswick, NJ, USA, July 1996.
  (ps)

• R. Di Cosmo and D. Kesner. Rewriting with extensional polymorphic lambda-calculus.
  Proc. of the 9th EACSL International Conference on Computer Science Logic (CSL).
  LNCS 1092, pages 215--232, Paderborn, Germany, September 1995.
  (ps)

• R. Di Cosmo and D. Kesner. Combining first order algebraic rewriting systems, recursion and extensional lambda-calculi.
  Proc. of the 21st Int. Colloquium on Automata, Languages and Programming (ICALP).
  LNCS 820, pages 462--472, Jerusalem, Israel, July 1994.
  (ps)

• D. Kesner. Reasoning about layered, wildcard and product patterns.
  Proc. of the 4th Int. Conference on Algebraic and Logic Programming (ALP).
  LNCS 850, pages 253--268, Madrid, Spain, September 1994.
  (ps)

• R. Di Cosmo and D. Kesner. A confluent reduction system for the extensional typed lambda-calculus with pairs, sum, recursion and terminal object.
  Proc. of the 20st Int. Colloquium on Automata, Languages and Programming (ICALP).
  LNCS 700, pages 645--656, Lund, Sweden, July 1993.
  (ps)

• D. Kesner and L. Puel and V. Tannen. A typed pattern calculus.
  Proc. of the 8th Annual IEEE Symposium on Logic in Computer Science (LICS).
  IEEE, pages 262--274, Montreal, Canada, June 1993.

• D. Kesner. Free sequentiality in orthogonal order-sorted rewriting systems with constructors.
  Proc. of the 11th Int. Conference on Automated Deduction (CADE).
  LNAI 607, pages 603--617, Saratoga Springs, NY, USA, June 1992.
  (ps)

• D. Kesner. Pattern matching in order-sorted languages.
  Proc. of the 16th Int. Symposium on Mathematical Foundations of Computer Science (MFCS).
  LNCS 520, pages 267--276, Kazimierz Dolny, Poland, September 1991.

Others

• D. Kesner and S. Yovine. 2018. LIA INFINIS: méthodes formelles pour la modélisation, la spécification, la vérification et le développement de logiciels.
  
  
• D. Kesner and S. Ó Conchúir. 2008. Milner's Lambda Calculus with Partial Substitutions.
  

• B. Jay and D. Kesner. 2008. Patterns as first-class citizens.