A Theory of Explicit Substitutions with Safe and Full Composition (2009)
Many different systems with explicit substitutions have been proposed to implement a large class of higher-order languages. Motivations and challenges that guided the development of such calculi in...
Resource operators for λ-calculus (2008)
Abstract We present a simple term calculus with an explicit control of erasure and duplication of substitutions, enjoying a sound and complete correspondence with the intuitionistic fragment of...
Roy Dyckhoff, Delia Kesner, Stéphane Lengr
Strong cut-elimination systems for
Roy Dyckhoff, Delia Kesner, Stéphane Lengr
Strong cut-elimination systems for
D'epartement de Math'ematiques et d'Informatique Ecole Normale Sup'erieure (2007)
Roberto Di Cosmo, Roberto Di Cosmo, Delia Kesner, Delia Kesner
Simulating expansions without expansions A propos de la simulation des expansions sans expansions
Combining Algebraic Rewriting, Extensional Lambda Calculi, and Fixpoints (2007)
Roberto Di Cosmo, Roberto Di, Delia Kesner
It is well known that confluence and strong normalization are preserved when combining algebraic rewriting systems with the simply typed lambda calculus. It is equally well known that confluence...
-calculi with explicit substitutions and composition which preserve fi-strong normalization (Extended
The theory of calculi with explicit substitutions revisited (2007)
Calculi with explicit substitutions are widely used in different areas of computer science such as functional and logic programming, proof-theory, theorem proving, concurrency, object-oriented...
The theory of calculi with explicit substitutions revisited (2007)
Calculi with explicit substitutions are widely used in different areas of computer science such as functional and logic programming, proof-theory, theorem proving, concurrency, object-oriented...
The theory of calculi with explicit substitutions revisited (2006)
Calculi with explicit substitutions are widely used in different areas of computer science such as functional and logic programming, proof-theory, theorem proving, concurrency, object-oriented...
The theory of calculi with explicit substitutions revisited (2006)
Calculi with explicit substitutions are widely used in different areas of computer science such as functional and logic programming, proof-theory, theorem proving, concurrency, object-oriented...
Patterns as first-class citizens (2006)
The pure pattern calculus generalises the pure lambda-calculus by basing computation on pattern-matching instead of beta-reduction. The simplicity and power of the calculus derive from allowing any...
Patterns as first-class citizens (2006)
The pure pattern calculus generalises the pure lambda-calculus by basing computation on pattern-matching instead of beta-reduction. The simplicity and power of the calculus derive from allowing any...
Roy Dyckhoff, Delia Kesner, Stéphane Lengr
Abstract. Inspired by the Curry-Howard correspondence, we study normalisation procedures in the depth-bounded intuitionistic sequent calculus of Hudelmaier (1988) for the implicational case, thus...
The theory of calculi with explicit substitutions revisited. Unpublished manuscript (2006)
Abstract. Calculi with explicit substitutions (ES) are widely used in different areas of computer science. Complex systems with ES were developed these last 15 years to capture the good computational...
The pure pattern calculus generalises the pure lambda-calculus by basing computation on pattern-matching instead of beta-reduction. The simplicity and power of the calculus derive from allowing any...
de Bruijn Indices for Metaterms (2005)
Bonelli, Eduardo, Kesner, Delia, Rios, Alejandro
In this paper we encode higher-order rewriting with names into higher-order rewriting in de Bruijn notation. This notation not only is defined for terms (as usually done in the literature) but also...
Relating Higher-order and First-order Rewriting (2005)
Bonelli, Eduardo, Kesner, Delia, Rios, Alejandro
We define a formal encoding from higher-order rewriting into first-order rewriting modulo an equational theory ℰ. In particular, we obtain a characterization of the class of higher-order...
• Syntax and Typing in λlxr • Reduction in λlxr (2004)
Delia Kesner, Stéphane Lengr, Connexion Λ-calculus
• Strong Normalisation of λlxr & Proof-nets modulo
Delia Kesner, Femke Van Raamsdonk, Joe Wells (eds, Issn Aachener, Informatik Berichte Aib
2004), which was held from May 31 through June 5, 2004, in Aachen. RDP 2004 consisted of the
Delia Kesner, Femke Van Raamsdonk, Joe Wells (eds, Issn Aachener, Informatik Berichte Aib
2004), which was held from May 31 through June 5, 2004, in Aachen. RDP 2004 consisted of the
From higher-order to first-order rewriting (2001)
Abstract. We show how higher-order rewriting may be encoded into first-order rewriting modulo an equational theory E. We obtain a characterization of the class of higher-order rewriting systems which...
Proof nets and explicit substitutions (2000)
Roberto Di Cosmo, Delia Kesner, Emmanuel Polonovski
We refine the simulation technique introduced in [10] to show strong normalization of-calculi with explicit substitutions via termination of cut elimination in proof nets [12]. We first propose a...
A de Bruijn notation for higher-order rewriting (2000)
Abstract. We propose a formalism for higher-order rewriting in de Bruijn notation. This notation not only is used for terms (as usually done in the literature) but also for metaterms, which are the...
A de Bruijn notation for higher-order rewriting (2000)
Abstract. We propose a formalism for higher-order rewriting in de Bruijn notation. This notation not only is used for terms (as usually done in the literature) but also for metaterms, which are the...
Proof Nets and Explicit Substitutions (2000)
Roberto Di Cosmo, Delia Kesner, Emmanuel Polonovski
We refine the simulation technique introduced in [10] to show strong normalization of -calculi with explicit substitutions via termination of cut elimination in proof nets [12]. We first propose a...
Proof Nets and Explicit Substitutions (2000)
Di Cosmo, Roberto, Kesner, Delia, Polonovski, Emmanuel
We refine the simulation technique introduced in [Di Cosmo and Kesner, 97] to show strong normalization of lambda-calculi with explicit substitutions via termination of cut elimination in linear...
Proof Nets and Explicit Substitutions (2000)
Di Cosmo, Roberto, Kesner, Delia, Polonovski, Emmanuel
We refine the simulation technique introduced in [Di Cosmo and Kesner, 97] to show strong normalization of lambda-calculi with explicit substitutions via termination of cut elimination in linear...
Pattern Matching as Cut Elimination (1999)
Serenella Cerrito, Delia Kesner
We present typed pattern calculus with explicit pattern matching and explicit substitutions, where both the typing rules and the reduction rules are modeled on the same logical proof system, namely...
Pattern Matching as Cut Elimination (1999)
Serenella Cerrito, Delia Kesner
We present a typed pattern calculus with explicit pattern matching and explicit substitutions, where both the typing rules and the reduction rules are modeled on the same logical proof system, namely...
Pattern Matching as Cut Elimination (1999)
Serenella Cerrito, Delia Kesner
We present a typed pattern calculus with explicit pattern matching and explicit substitutions, where both the typing rules and the reduction rules are modeled on the same logical proof system, namely...
Explicit Substitutions for Objects and Functions (1998)
This paper proposes an implementation of objects and functions via a calculus with explicit substitutions which is confluent and preserves strong normalization. The source calculus corresponds to the...
Strong normalization of explicit substitutions via cut elimination in proof nets (1997)
Roberto Di Cosmo, Delia Kesner
In this paper, we show the correspondence existing between normalization in calculi with explicit substitution and cut elimination in sequent calculus for Linear Logic,via Proof Nets. This...
Reducing AC-Termination to Termination (1997)
We present a new technique for proving AC-termination. We show that if certain conditions are met, AC-termination can be reduced to termination, i. e., termination of a TRS S modulo an AC-theory can...
) Delia Kesner CNRS and LRI, B at 490, Universit e Paris-Sud - 91405 Orsay Cedex, France. e-mail:Delia.Kesner@lri.fr Abstract. This paper studies confluence properties of extensional and...
This paper studies preservation of fi-strong normalization by two different confluent -calculi with explicit substitutions defined in [Kes96]; the particularity of these calculi, called d and dn...
A Typed Pattern Calculus (1996)
Delia Kesner, Laurence Puel, Val Tannen
The theory of programming with pattern-matching function definitions has been studied mainly in the framework of first-order rewrite systems. We present a typed functional calculus that emphasizes...
Rewriting with Extensional Polymorphic lambda-calculus (1996)
Roberto Di Cosmo, Delia Kesner
. We provide a confluent and strongly normalizing rewriting system, based on expansion rules, for the extensional second order typed lambda calculus with product and unit types: this system...
Combining First Order Algebraic Rewriting Systems, Recursion and Extensional Lambda Calculi (1994)
Roberto Di Cosmo, Delia Kesner
It is well known that confluence and strong normalization are preserved when combining left-linear algebraic rewriting systems with the simply typed lambda calculus. It is equally well known that...
Combining First Order Algebraic Rewriting Systems, Recursion and Extensional Lambda Calculi (1994)
Roberto Di Cosmo, Delia Kesner
It is well known that confluence and strong normalization are preserved when combining left-linear algebraic rewriting systems with the simply typed lambda calculus. It is equally well known that...
Reasoning about Layered, Wildcard and Product Patterns (1994)
We study the extensional version of the simply typed -calculus with product types and fixpoints enriched with layered, wildcard and product patterns. Extensionality is expressed by the surjective...
Roberto Di Cosmo, Delia Kesner
We add extensional equalities for the functional and product types to the typed -calculus with not only products and terminal object, but also sums and bounded recursion (a version of recursion that...
Simulating Expansions Without Expansions (1993)
Roberto Di Cosmo, Delia Kesner
ion) Let M : A 2 be a term where the variable x : A 1 may occur free. If for every N 2 REDA 1 we have M [N=x] 2 REDA 2 , then x : A 1 :M 2 REDA 1 !A 2 . Proof. We want to show that (x:M)P is...
A Typed Pattern Calculus (1993)
Abstract. The pure pattern calculus generalises the pure lambda-calculus by basing computation on pattern-matching instead of beta-reduction. The simplicity and power of the calculus derive from...
Free Sequentiality in Orthogonal Order-Sorted Rewriting Systems with Constructors (1992)
We introduce the notions of sequentiality and strong sequentiality in ordersorted rewriting systems, both closely related to the subsort order and to the form of declarations of the signature. We...
Pattern Matching in Order-Sorted Languages (1991)
We study the problem of pattern matching in order-sorted languages whose evaluation strategy is lazy. We propose an extension of the Puel-Suarez compilation scheme to function definitions via...
Pattern Matching in Order-Sorted Languages (1991)
This work was initiated by the author while she was a research intern at Digital’s Paris Research Laboratory from April to September 1990 working on her stage de DEA for the Universitéde Paris 7....
Confluence of Extensional and Non-Extensional λ-calculi with Explicit Substitutions
This paper studies confluence of extensional and non-extensional -calculi with explicit substitutions, where extensionality is interpreted by j-expansion. For that, we propose a scheme for explicit...