Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Delia Kesner: Selected Papers

Selected Papers


The Theory of Explicit Substitutions Revisited
Delia Kesner

ps file
Proceedings of the 16th EACSL Annual Conference on Computer Science and Logic (CSL)
LNCS, Lausanne, Switzerland, September 2007.
© Springer-Verlag          


Strong cut-elimination systems for Hudelmaier's depth-bounded sequent calculus for implicational logic
Roy Dyckhoff and Delia Kesner and Stéphane Lengrand

Proceedings of the third International Joint Conference on Automated Reasoning (IJCAR)
LNCS, Seattle, USA, August 2006.
(ps file) © Springer-Verlag          


Pure pattern calculus
C. Barry Jay and Delia Kesner

Proceedings of the European Symposium on Programming (ESOP)
LNCS 3924, pages 100-114, Vienna, Austria, March-April 2006.
(ps file) © Springer-Verlag

A second solution is presented as:
Patterns as first-class citizens
Ps file

Extending the Explicit Substitution Paradigm
Delia Kesner and Stéphane Lengrand

Proceedings of the 16th International Conference on Rewriting Techniques and Applications (RTA)
LNCS 3467, pages 407-422, Nara, Japan, April 2005.
(ps file) © Springer-Verlag          

A long version is:
Resource Operators for lambda-calculus
Information and Computation. 205(4):419-473, 2007.

Expression Reduction Systems and Extensions: An Overview
John Glauert and Delia Kesner and Zurab Khasidashvili

In Festschrift in Honor of Jan Willem Klop
Processes, Terms and Cycles: Steps on the Road to Infinity
LNCS 3838, pages 496-553, 2005.


Expression Reduction Systems with Patterns
Julien Forest and Delia Kesner

Proceedings of the 14th International Conference on Rewriting Techniques and Applications (RTA)
LNCS 2706, pages 107-122, Valencia, Spain, June 2003.
(ps file)© Springer-Verlag

A long version is:
Expression Reduction Systems with Patterns
To appear in Journal of Automated Reasoning.


From Higher-Order to First-Order Rewriting
Eduardo Bonelli and Delia Kesner and Alejandro Ríos

Proceedings of the 12th International Conference on Rewriting Techniques and Applications (RTA)
LNCS 2051, pages 47--62, Utrecht, The Netherlands, June 2001.

A long version is:
Relating Higher-Order and First-Order Rewriting
Journal of Logic and Computation. 15: 901-947, 2005.


A de Bruijn notation for higher-order rewriting
Eduardo Bonelli and Delia Kesner and Alejandro Ríos

Proceedings of the 11th International Conference on Rewriting Techniques and Applications (RTA)
LNCS 1833, pages 62--79, Norwick, UK, July 2000.
(ps file)© Springer-Verlag

A long version is:
de Bruijn Indices for MetaTerms
Journal of Logic and Computation. 15: 855-899, 2005.


Proof Nets and Explicit Substitutions
Roberto Di Cosmo and Delia Kesner and Emmanuel Polonovski

Foundations of Software Science and Computation Structures (FOSSACS)
LNCS 1784, pages 63--81, Berlin, Germany, March/April, 2000.

A long version iss:
Proof Nets and Explicit Substitutions
Mathematical Structures in Computer Science. 13(3): 409-450, 2003.


Pattern Matching as Cut Elimination
Serenella Cerrito and Delia Kesner

Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science (LICS)
pages 98-108, Trento, Italy, July 1999.
(ps file)© IEEE

A long version is as:
Pattern Matching as Cut Elimination
Theoretical Computer Science. 323:71-127, 2004.


Explicit Substitutions for Objects and Functions
Delia Kesner and Pablo E. Martínez López

Proceedings of the Joint International Symposiums
Programming Languages, Implementations, Logics and Program (PLILP) and Algebraic and Logic Programming (ALP)
LNCS 1490, pages 195-212, Pisa, Italy, September 1998.

A long version is:
Explicit Substitutions for Objects and Functions
The Journal of Functional and Logic Programming
Special Issue 2, Volume 1999
Published by The MIT Press


Reducing AC-Termination to Termination
Maria Ferreira and Delia Kesner and Laurence Puel

Proceedings of the 23rd International Symposium on Mathematical Foundations of Computer Science (MFCS)
LNCS 1450, pages 239-247, Brno, Czech Republic, August 1998.
(ps file)© Springer-Verlag


Strong Normalization of Explicit Substitutions via Cut Elimination in Proof Nets
Roberto Di Cosmo and Delia Kesner

Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science (LICS)
pages 35-45, Warsaw, Poland, July 1997.
(ps file) © IEEE


Lambda-calculi with explicit substitutions and composition which preserve beta-strong normalization (Extended Abstract)
Maria Ferreira and Delia Kesner and Laurence Puel

Proceedings of the 5th International Conference on Algebraic and Logic Programming (ALP)
LNCS 1139, pages 284-298, Aachen, Germany, September 1996.
(ps file)© Springer-Verlag

A long version is:
Lambda-calculi with Explicit Substitutions Preserving Strong Normalization
Applicable Algebra in Engineering, Communication and Computing. 9(4): 333-371, 1999.


Confluence properties of extensional and non-extensional lambda-calculi with explicit substitutions
Delia Kesner

Proceedings of the 7th International Conference on Rewriting Techniques and Applications (RTA)
LNCS 1103, pages 184-199, New Brunswick, NJ, USA, July 1996.
(ps file)© Springer-Verlag

A long version is:
Confluence of Extensional and Non-Extensional lambda-calculi with Explicit Substitutions
Theoretical Computer Science. 238(1-2): 183-220, 2000.


Rewriting with extensional polymorphic lambda-calculus
Roberto Di Cosmo and Delia Kesner

Proceedings of the 9th International Workshop on Computer Science Logic (CSL)
LNCS 1092, pages 215-232, Paderborn, Germany, September 1995.
(ps file)© Springer-Verlag


Combining first order algebraic rewriting systems, recursion and extensional lambda-calculi
Roberto Di Cosmo and Delia Kesner

Proceedings of the 21st International Colloquium on Automata, Languages and Programming (ICALP)
LNCS 820, pages 462-472, Jerusalem, Israel, July 1994.
(ps file)© Springer-Verlag

A long version is:
Combining algebraic rewriting systems, extensional lambda-calculi and fixpoints
Theoretical Computer Science
169: 201-220, 1996.


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

A long version is:
A typed pattern calculus
Information and Computation. 124(1):32-61, 1995.


A confluent reduction system for the extensional typed lambda-calculus with pairs, sum, recursion and terminal object
Roberto Di Cosmo and Delia Kesner

Proceedings of the 20st International Colloquium on Automata, Languages and Programming (ICALP)
LNCS 700, pages 645-656, Lund, Sweden, July 1993.
(ps file)© Springer-Verlag

A long version is:
Simulating expansions without expansions
Mathematical Structures in Computer Science. 4: 315-362, 1994.


Reasoning about layered, wildcard and product patterns
Delia Kesner

Proceedings of the 4th International Conference on Algebraic and Logic Programming (ALP)
LNCS 850, pages 253-268, Madrid, Spain, September 1994.
( ps file)© Springer-Verlag

A long version is:
Reasoning about redundant patterns
Delia Kesner
Journal of Functional and Logic Programming. Number 4, 1997.


Free sequentiality in orthogonal order-sorted rewriting systems with constructors
Delia Kesner

Proceedings of the 11th International Conference on Automated Deduction (CADE)
LNAI 607, pages 603-617, Saratoga Springs, NY, USA, June 1992.
(ps file)© Springer-Verlag


Pattern matching in order-sorted languages
Delia Kesner

Proceedings of the 16th International Symposium on Mathematical Foundations of Computer Science (MFCS)
LNCS 520, pages 267-276, Kazimierz Dolny, Poland, September 1991.