On Isomorphisms of Intersection Types (2009)
Mariangiola Dezani-ciancaglini, Roberto Di Cosmo, Elio Giovannetti, Makoto Tatsuta
Abstract. The study of type isomorphisms for different λ-calculi started over twenty years ago, and a very wide body of knowledge has been established, both in terms of results and in terms of...
Docteur En Informatique, Boris Yakobowski, Roberto Di Cosmo, Stéphanie Weirich, Hugo Herbelin, ...
pour obtenir le titre de
Boris Yakobowski, Roberto Di Cosmo, Stéphanie Weirich, Hugo Herbelin, Fritz Henglein, ...
présentée à
Strong Normalization of Proof NetsModulo Structural Congruences (2009)
Abstract. This paper proposes a notion of reduction for the proof nets of LinearLogic modulo an equivalence relation on the contraction links, that essentially amounts to consider the contraction as...
Since March 1998, the original French version of this text has been available at
Roberto Di Cosmo, Berke Durak, Xavier Leroy, Fabio Mancinelli
Abstract. In the mainstream adoption of free and open source software (FOSS), distribution editors play a crucial role: they package, integrate and distribute a wide variety of software, written in a...
Trampa en el Cyberespacio[+] (2008)
Durante las últimas vacaciones de Navidad me he quedado asombradísimo con la fascinación creciente de los medios de comunicación por ese oscuro objeto del deseo que se oculta detrás de las...
Security and Protection. (2008)
* May 1985: short internal memory on Robinson's Unification Theorem and Type Assignment for pure *-calculus, (this included an implementation of the unification algorithm for type inference both...
INRIA-Roquencourt Abstract (2008)
Marcelo Fiore, Roberto Di Cosmo, Vincent Balat
Tarski asked whether the arithmetic identities taught in high school are complete for showing all arithmetic equations valid for the natural numbers. The answer to this question for the language of...
MAP: A Formal Calculus on Data-parallel Applications over n-dimensional Dense Arrays (2008)
Roberto Di Cosmo, Zheng Li, Susanna Pelagatti
Data-parallel applications over multidimensional dense arrays have always been an important application area of numerical computing. Based on popular parallel programming models like PVM and MPI, a...
Subtyping Recursive Types modulo AssociativeCommutative Products (2008)
1 Introduction The study of type isomorphisms is concerned with identifying data types by abstract-ing away from irrelevant details in the syntax of types, or--in other words--irrelevant choices in...
Subtyping Recursive Types modulo AssociativeCommutative Products (2008)
1 Introduction The study of type isomorphisms is concerned with identifying data types by abstract-ing away from irrelevant details in the syntax of types, or--in other words--irrelevant choices in...
UNIVERSITÀ DI PISA Ecole Doctorale de Sciences Mathématiques de Paris Centre (2008)
Doctorat En Informatique, Stefano Galatolo, Olivier Bournez, Abbas Edalat, Peter Gács, Olivier Bournez, ...
Mathieu HOYRUP Calculabilité, aléatoire et théorie ergodique sur les espaces métriques Calcolabilità, aleatorio e teoria ergodica in spazi metrici Thèse dirigée par
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
Semantique Dea, Semantique Dea, Roberto Di Cosmo, Roberto Di Cosmo, Roberto Di Cosmo
Definitions des langages de programmation Dans la definition d'un langage de programmation, on rencontre plusieurs types de di#cultes, liees a des aspects assez di#erents, dont les plus...
Application of Functional Languages to Massive and Complex Computational Problems (2007)
ion: Nets . . . . . . . . . . . . . . . . . . . . . 50 4.4.1 Net Signature . . . . . . . . . . . . . . . . . . . . . . . 51 4.4.2 Packet Signature . . . . . . . . . . . . . . . . . . . . . 53 4.4.3...
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...
LIENS-DMI Ecole Normale Sup erieure (2007)
Marco Danelutto, Roberto Di Cosmo, Xavier Leroy, Inria Roquencourt, Domaine De Voluceau, Susanna Pelagatti
# The OcamlP3l system has been partially funded by the Galileo bilateral France-Italy project n.97029 1 Writing parallel programs is not easy, and debugging them is usually a nightmare. To cope with...
Managing the Complexity of Large Free and Open Source Package-Based Software Distributions (2006)
Fabio Mancinelli, Jaap Boender, Roberto Di Cosmo, Jérôme Vouillon, Berke Durak, Xavier Leroy
The widespread adoption of Free and Open Source Software (FOSS) in many strategic contexts of the information technology society has drawn the attention on the issues regarding how to handle the...
Subtyping recursive types modulo associative commutative products (2005)
Roberto Di Cosmo, Franois Pottier, Didier Rmy
We study subtyping of recursive types in the presence of associative and commutative products---that is, subtyping modulo a restricted form of type isomorphisms. We show that this relation, which we...
Subtyping recursive types modulo associative commutative products (2005)
Roberto Di Cosmo, Franois Pottier, Didier Rmy
We study subtyping of recursive types in the presence of associative and commutative products---that is, subtyping modulo a restricted form of type isomorphisms. We show that this relation, which we...
Subtyping recursive types modulo associative commutative products (2005)
Roberto Di Cosmo, François Pottier, Didier Rémy
Abstract. This work sets the formal bases for building tools that help retrieve classes in object-oriented libraries. In such systems, the user provides a query, formulated as a set of class...
Subtyping recursive types modulo associative commutative products (2005)
Roberto Di Cosmo, François Pottier, Didier Rémy
Abstract. This work sets the formal bases for building tools that help retrieve classes in object-oriented libraries. In such systems, the user provides a query, formulated as a set of class...
Eligiendo la herramienta legal correcta para proteger el software (2003)
este artículo investiga los méritos relativos de las diferentes herramientas legales para proteger el software, en el justo momento en que la Unión Europea está considerando cambiar su política...
Subtyping Recursive Types modulo Associative Commutative Products (2003)
Roberto Di Cosmo, Francois Pottier, Didier Remy
This work sets the formal bases for building tools to retrieve classes in object-oriented libraries. In such systems, the user provides a query, formulated as a set of class interfaces, and the tool...
Remarks on isomorphisms in typed lambda calculi with empty and sum types (2002)
Marcelo Fiore, Roberto Di Cosmo
Tarski asked whether the arithmetic identities taught in high school are complete for showing all arithmetic equations valid for the natural numbers. The answer to this question for the language of...
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)
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 Linear Logical View of Linear Type Isomorphisms (1999)
Vincent Balat, Roberto Di Cosmo
. The notion of isomorphisms of types has many theoretical as well as practical consequences, and isomorphisms of types have been investigated at length over the past years. Isomorphisms in weak...
Strong Normalization of Proof Nets Modulo Structural Congruences (1999)
Roberto Di Cosmo, Stefano Guerrini
. This paper proposes a notion of reduction for the proof nets of Linear Logic modulo an equivalence relation on the contraction links, that essentially amounts to consider the contraction as an...
OcamlP3l a functional parallel programming system (1998)
Uperieure S Ormale, N Ecole, Roberto Di Cosmo, Roberto Di Cosmo, Xavier Leroy, Xavier Leroy, ...
Writing parallel programs is not easy, and debugging them is usually a nightmare. To cope with these difficulties, a structured approach to parallel programs using skeletons and template based...
Parallel Functional Programming with Skeletons: the ocamlp3l experiment (1998)
Marco Danelutto, Roberto Di Cosmo, Xavier Leroy, Susanna Pelagatti
Writing parallel programs is not easy, and debugging them is usually a nightmare. To cope with these difficulties, a structured approach to parallel programs using skeletons and template based...
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...
On Modular Properties of Higher Order Extensional Lambda Calculi (1997)
Roberto Di Cosmo, Neil Ghani, Roberto Di, Cosmo Neil Ghani, Ecole Normale Superieure
. We prove that confluence and strong normalisation are both modular properties for the addition of algebraic term rewriting systems to Girard's F ! equipped with either fi-equality or...
On the Power of Simple Diagrams (1996)
. In this paper we focus on a set of abstract lemmas that are easy to apply and turn out to be quite valuable in order to establish confluence and/or normalization modularly, especially when adding...
A Brief History of Rewriting With Extensionality (1996)
Roberto Di Cosmo, Ecole Normale Superieure, Roberto Di, Cosmo Glasgow, M) M
<F NaN><F NaN> A A ×B<F NaN><F NaN> oo # 1<F NaN><F NaN> // # 2 B That is: h = #f, g# = ## 1 # h, # 2 # h# Case C A<F NaN><F NaN> // in 1<F...
Sémantique Dénotationnelle (1996)
Semantique Dea, Semantique Dea, Roberto Di Cosmo, Roberto Di Cosmo, Roberto Di Cosmo
ui n'est plus ambigu + @ @ @ @ @ @ @ a + > > > > > > > > ~ ~ ~ ~ ~ ~ ~ ~ b c ## + > > > > > > > > ~ ~ ~ ~ ~ ~ ~ + @ @ @ @ @ @ @ @...
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...
Expanding Extensional Polymorphism (1995)
Roberto Di Cosmo, Adolfo Piperno
. We prove the confluence and strong normalization properties for second order lambda calculus equipped with an expansive version of j-reduction. Our proof technique, based on a simple abstract lemma...
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...
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...
Provable Isomorphisms of Types (1990)
Kim B. Bruce, Roberto Di Cosmo, Giuseppe Longo
A constructive characterization is given of the isomorphisms which must hold in all models of the typed lambda calculus with surjective pairing. Work of Rittri (1989) on using types as search keys in...