Publications
Book chapters
J. Glauert and
D. Kesner
and Z. Khasidashvili
Expression Reduction Systems and Extensions: An Overview
In Festschrift in Honor of Jan Willem Klop
Processes, Terms and Cycles: Steps on the Road to Infinity
LNCS 3838,
pages 496553, 2005.
Journals

J. Espírito Santo and
D. Kesner and
L. Peyrot.
A Faithful and Quantitative Notion of Distant Reduction for the LambdaCalculus 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), 20(2):152, 2024.

D. Kesner and
L. Peyrot and
D. Ventura.
Node Replication: Theory and Practice.
Logical Methods in Computer Science (LMCS), 20(1):166, 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 FineGrained Computational Interpretation of Girard's Intuitionistic ProofNets.
Proc. of the ACM on Programming Languages Journal (PACMPL), 6(POPL):8:18:28, 2022.
 A. Bucciarelli
and D. Kesner
and
S. Ronchi Della Rocca.
Solvability=Typability+Inhabitation.
Logical Methods in Computer Science (LMCS), 17(1):127, 2021.

B. Accattoli and
S. GrahamLengrand and D. Kesner.
Tight Typings and Split Bounds, Fully Developed.
Journal of Functional Programming (JFP), 30(14):185, 2020.

D. Kesner and
P. Vial.
Nonidempotent types for classical calculi in natural deduction style.
Logical Methods in Computer Science (LMCS), 16(1):146, 2020.
 D. Kesner and
D. Ventura.
A resource aware semantics for a focused intuitionistic calculus.
Mathematical Structures in Computer Science (MSCS), 29(1):93126, 2019 (published online 22 May 2017).

B. Accattoli and
S. GrahamLengrand and D. Kesner.
Tight Typings and Split Bounds.
Proc. of the ACM on Programming Languages Journal (PACMPL), 2(ICFP):94:194:30, 2018.
 A. Bucciarelli and
D. Kesner and
S. Ronchi Della Rocca.
Inhabitation for Intersection Types.
Logical Methods in Computer Science (LMCS), 14(3):128, 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:120:29, 2017.
 A. Bucciarelli and
D. Kesner and
D. Ventura.
NonIdempotent Intersection Types for the LambdaCalculus.
Logic Journal of the IGPL, 25(4):431464, 2017.

E. Bonelli and D. Kesner
and C. Lombardi and A. Ríos.
On abstract normalisation
beyond neededness.
Theoretical Computer Science (TCS), 672:3663, 2017.
 B. Accattoli
and D. Kesner.
Preservation of strong normalisation modulo permutations for the
structural calculus.
Logical Methods in Computer Science (LMCS), 8(1):144, 2012.

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

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

B. Jay and
D. Kesner.
Firstclass patterns.
Journal of Functional Programming (JFP), 19(2): 191225, 2009.
 J. Forest and
D. Kesner.
Expression Reduction Systems with Patterns.
Journal of Automated Reasoning (JAR), 39(4):513541, 2007.
 D. Kesner and
S. Lengrand.
Resource Operators for lambdacalculus.
Information and Computation (I&C), 205(4):419473, 2007.

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

E. Bonelli and
D. Kesner and
A. Ríos.
Relating HigherOrder and FirstOrder Rewriting.
Journal of Logic and Computation (JLC), 15(6): 901947, 2005.

S. Cerrito and
D. Kesner.
Pattern Matching as Cut Elimination.
Theoretical Computer Science (TCS), 323(13):71127, 2004.

R. Di Cosmo and
D. Kesner and
E. Polonovski.
Proof Nets and Explicit Substitutions.
Mathematical Structures in Computer Science (MSCS), 13(3): 409450, 2003.
 D. Kesner.
Confluence of Extensional and NonExtensional
lambdacalculi with Explicit Substitutions.
Theoretical Computer Science (TCS),
238(12): 183220, 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:133, Vol 1999.
 M. Ferreira and
D. Kesner
and
L. Puel.
Lambdacalculi with Explicit Substitutions Preserving Strong Normalization.
Applicable Algebra in Engineering, Communication and Computing (AAECC),
9(4): 333371, 1999.
 D. Kesner.
Reasoning about redundant patterns.
Journal of Functional and Logic Programming (JLFP), Number 4:348, Vol 1997.
 R. Di Cosmo and
D. Kesner.
Combining algebraic rewriting systems,
extensional lambdacalculi and fixpoints.
Theoretical Computer Science (TCS),
169(2): 201220, 1996.
 D. Kesner and
L. Puel and
V. Tannen.
A typed pattern calculus.
Information and Computation (I&C), 124(1):3261, 1995.
 R. Di Cosmo and
D. Kesner.
Simulating expansions without expansions.
Mathematical Structures in Computer Science (MSCS), 4(3): 315362, 1994.
Conferences

V. Arrial and
D. Kesner and
G. Guerrieri.
Genericity Through Stratification.
Proc. of the 39th of the ACM/IEEE Symposium on Logic in Computer Science (LICS).
ACM, Tallinn, Estonia, July 2024, to appear.
(pdf)

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 5368, 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:118: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:125: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 344364, Luxembourg, Luxembourg, MarchApril 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 619632, 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 1332, 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:14:23, Barcelona, Spain, January 2020.
(pdf)

S. Alves and
D. Kesner and
D. Ventura.
A Quantitative Understanding of Pattern Matching.
PostProc of the 25th International Conference on Types for Proofs and Programs (TYPES).
LIPIcs, Vol 175, pages 3:13:36, Oslo, Norway, June 2019.
(pdf)
 D. Kesner and
A. Ríos and A. Viso.
Callbyneed, neededness and all that.
Proc. of the 20th Int. Conference on Foundations of Software Science and Computation Structures (FoSSaCS).
LNCS 10803, pages 241257, 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:124:17,
Oxford, UK, September 2017.
(pdf)
 D. Kesner.
Reasoning about callbyneed by means of types.
Proc. of the 19th Int. Conference on Foundations of Software Science and Computation Structures (FoSSaCS).
LNCS 9634, pages 424441, 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 7591, 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 116,
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 123137,
Warsaw, Poland, July 2015.
(pdf)

F. L. C. de Moura and
D. Kesner and
M. AyalaRincó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 391402,
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 296310,
Rome, Italy, September 2014.
(pdf)

A. Bucciarelli and
D. Kesner and
S. Ronchi Della Rocca.
The Inhabitation Problem for NonIdempotent Intersection Types.
Proc. of the 8th Int. Conference on Theoretical Computer Science (TCS).
LNCS 8705, pages 341354
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 SIGPLANSIGACT Symposium on Principles of Programming Languages (POPL).
ACM, pages 659670, 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 117132,
Nagoya, Japan, MayJune 2012.
(pdf)
 B. Accattoli
and D. Kesner.
The permutative lambdacalculus.
Proc. of the 18th Int. Conference on Logic for Programming Artificial Intelligence and
Reasoning (LPAR).
LNCS 7180,
pages 2336,
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 HigherOrder Rewriting (HOR 2010).
EPTCS, Number 49, pages 5872, Edinburgh, United Kingdom, July 2011.
 B. Accattoli
and D. Kesner.
The structural lambdacalculus.
Proc. of the 19th EACSL International Conference on Computer Science and Logic (CSL).
LNCS 6247, pages 381395,
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 464476,
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 311322,
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 238252,
Lausanne, Switzerland, September 2007.
(pdf)
 R. Dyckhoff and
D. Kesner and
S. Lengrand.
Strong cutelimination systems for Hudelmaier's
depthbounded sequent calculus for implicational logic.
Proc. of the 3rd Int. Joint Conference on Automated Reasoning (IJCAR).
LNAI 4130, pages 347361,
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 100114,
Vienna, Austria, MarchApril 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 407422, 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 107122, Valencia, Spain, June 2003.
(ps)

E. Bonelli and
D. Kesner and
A. Ríos.
From HigherOrder to FirstOrder Rewriting.
Proc. of the 12th Int.
Conference on Rewriting Techniques and Applications (RTA).
LNCS 2051, pages 4762, Utrecht, The Netherlands, June 2001.
(ps)

E. Bonelli and
D. Kesner and
A. Ríos.
A de Bruijn notation for higherorder rewriting.
Proc. of the 11th Int.
Conference on Rewriting Techniques and Applications (RTA).
LNCS 1833,
pages 6279, 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 6381, 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 98108, 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 195212, Pisa, Italy, September 1998.
 M. Ferreira and
D. Kesner
and
L. Puel.
Reducing ACTermination to Termination.
Proc. of the 23rd Int. Symposium on Mathematical
Foundations of Computer Science (MFCS).
LNCS 1450,
pages 239247, 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 3545, Warsaw, Poland, July 1997.
(ps)
 M. Ferreira and
D. Kesner
and L. Puel.
Lambdacalculi with explicit substitutions and composition which
preserve betastrong normalization (Extended Abstract).
Proc. of the 5th Int. Conference on Algebraic
and Logic Programming (ALP).
LNCS 1139,
pages 284298, Aachen, Germany, September 1996.
(ps)
 D. Kesner.
Confluence properties of extensional and nonextensional
lambdacalculi with explicit substitutions.
Proc. of the 7th Int.
Conference on Rewriting Techniques and Applications (RTA).
LNCS 1103, pages 184199,
New Brunswick, NJ, USA, July 1996.
(ps)
 R. Di Cosmo and
D. Kesner.
Rewriting with extensional polymorphic lambdacalculus.
Proc. of the 9th EACSL International Conference on
Computer Science Logic (CSL).
LNCS 1092, pages 215232,
Paderborn, Germany, September 1995.
(ps)
 R. Di Cosmo and
D. Kesner.
Combining first order algebraic rewriting systems, recursion
and extensional lambdacalculi.
Proc. of the 21st Int. Colloquium on
Automata, Languages and Programming (ICALP).
LNCS 820, pages 462472,
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 253268,
Madrid, Spain, September 1994.
(ps)
 R. Di Cosmo and
D. Kesner.
A confluent reduction system for the extensional typed lambdacalculus
with pairs, sum, recursion and terminal object.
Proc. of the 20st Int. Colloquium on
Automata, Languages and Programming (ICALP).
LNCS 700, pages 645656,
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 262274, Montreal, Canada, June 1993.
 D. Kesner.
Free sequentiality in orthogonal ordersorted rewriting systems
with constructors.
Proc. of the 11th Int. Conference on Automated
Deduction (CADE).
LNAI 607, pages 603617,
Saratoga Springs, NY, USA, June 1992.
(ps)
 D. Kesner.
Pattern matching in ordersorted languages.
Proc. of the 16th Int. Symposium on Mathematical
Foundations of Computer Science (MFCS).
LNCS 520, pages 267276,
Kazimierz Dolny, Poland, September 1991.
Others