Delia Kesner: Publications

Book chapters

Journals

• B. Accattoli and D. Kesner. Preservation of strong normalisation modulo permutations for the structural calculus.
  Submitted.
  

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

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

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

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

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

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

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

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

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

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

• D. Kesner and P. E. Martínez López. Explicit Substitutions for Objects and Functions.
  The Journal of Functional and Logic Programming (MIT Press). Special Issue 2, Volume 1999.

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

• D. Kesner. Reasoning about redundant patterns.
  D. Kesner. Journal of Functional and Logic Programming. Number 4, 1997.

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

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

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

Conferences

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

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

• D. Kesner and F. Renaud. The prismoid of resources.
  Proceedings 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) © Springer-Verlag.

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

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

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

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

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

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

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

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

• R. Di Cosmo and D. Kesner and E. Polonovski. Proof Nets and Explicit Substitutions.
  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.
  Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science (LICS).
  pages 98-108, Trento, Italy, July 1999.
  (ps)© IEEE

• D. Kesner and P. E. Martínez López. Explicit Substitutions for Objects and Functions.
  Proceedings 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.
  Proceedings of the 23rd Int. Symposium on Mathematical Foundations of Computer Science (MFCS).
  LNCS 1450, pages 239-247, Brno, Czech Republic, August 1998.
  (ps)© Springer-Verlag.

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

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

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

• R. Di Cosmo and D. Kesner. Rewriting with extensional polymorphic lambda-calculus.
  Proceedings of the 9th Int. Workshop on Computer Science Logic (CSL).
  LNCS 1092, pages 215-232, Paderborn, Germany, September 1995.
  (ps)© Springer-Verlag.

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

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

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

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

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

• D. Kesner. Pattern matching in order-sorted languages.
  Proceedings 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 C. Lombardi and A. Ríos. 2010. A Standardisation proof for algebraic pattern calculi.
  

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