A Conditional Logical Framework ⋆ (2009)
Furio Honsell, Marina Lenisa, Luigi Liquori, Ivan Scagnetto
Abstract. The Conditional Logical Framework LFK is a variant of the Harper-Honsell-Plotkin’s Edinburgh Logical Framemork LF. It features a generalized form of λ-abstraction where β-reductions...
IOS Press A Subtyping for Extensible, Incomplete Objects To Helena Rasiowa: in memoriam (2008)
Viviana Bono, Michele Bugliesi, Mariangiola Dezani-ciancaglini, Luigi Liquori
Abstract. We extend the type system for the Lambda Calculus of Objects [16] with a mechanism of width subtyping and a treatment of incomplete objects. The main novelties over previous work are the...
Abstract Intersection-Types à la Church (2008)
Luigi Liquori, Inria Sophia Antipolis, Simona Ronchi, Della Rocca
In this paper, we present Λ t ∧, a fully typed λ-calculus based on the intersection-type system discipline, which is a counterpart à la Church of the type assignment system as invented by Coppo...
Steffen Bakel, Luigi Liquori, Simona Ronchi, Rocca Paweł Urzyczyn, Afdeling Informatica, Instytut Informatyki
We study the cube of type assignment systems, as introduced in [10]. This cube is obtained from Barendregt’s typed-cube [1] via a natural type erasing function E, that erases type information from...
Rewrite Strategies in the Rewriting Calculus Abstract (2008)
Horatiu Cirstea, Claude Kirchner, Luigi Liquori, Benjamin Wack
This paper presents an overview on the use of the rewriting calculus to express rewrite strategies. We motivate first the use of rewrite strategies by examples in the ELAN language. We then show how...
Abstract Object Calculi in Linear Logic (2008)
Michele Bugliesi, Giorgio Delzanno, Luigi Liquori, Maurizio Martelli
Several calculi of objects have been studied in the recent literature, that support the central features of object-based languages: messages, inheritance, dynamic dispatch, object update and...
Comparing Cubes of Typed and Type Assignment Systems (2008)
Steffen Bakel, Luigi Liquori, Simona Ronchi Rocca, Paweł Urzyczyn, Instytut Informatyki, Uniwersytetu Warszawskiego, ...
We study the cube of type assignment systems, as introduced in [13], and confront it with Barendregt’s typed-cube [4]. The first is obtained from the latter through applying a natural type erasing...
Towards an Intersection Typed System à la Church (2008)
Luigi Liquori, Simona Ronchi, Della Rocca
Abstract In this paper, we presents a comfortable fully typed lambda calculus based on the well-known intersection type system discipline where proof are not only feasible but easy; the present...
Rewrite Strategies in the Rewriting Calculus Abstract (2008)
Horatiu Cirstea, Claude Kirchner, Luigi Liquori, Benjamin Wack
This paper presents an overview on the use of the rewriting calculus to express rewrite strategies. We motivate first the use of rewrite strategies by examples in the ELAN language. We then show how...
Alberto Ciaffaglione, Luigi Liquori, Marino Miculan
Abstract. We illustrate a methodology for formalizing and reasoning about Abadi and Cardelli’s object-based calculi, in (co)inductive type theory, such as the Calculus of (Co)Inductive...
Luigi Liquori, Furio Honsell, Rekha Redamalla
In this paper we develop the language theory underpinning the logical framework PLF. This language features lambda abstraction with patterns and application via pattern-matching. Reductions are...
Reasoning about Object-based Calculi in (Co)Inductive Type Theory and the Theory of Contexts (2008)
Alberto Ciaffaglione, Luigi Liquori, Marino Miculan
Abstract. We illustrate a methodology for formalizing and reasoning about Abadi and Cardelli’s object-based calculi, in (co)inductive type theory, such as the Calculus of (Co)Inductive...
ABSTRACT Pure Patterns Type Systems (2008)
Gilles Barthe, Horatiu Cirstea, Claude Kirchner, Luigi Liquori
We introduce a new framework of algebraic pure type systems in which we consider rewrite rules as lambda terms with patterns and rewrite rule application as abstraction application with built-in...
• Projet(s) de recherche: Mascotte (2008)
Luigi Liquori, Projet Mascotte, Stage Ensl
This work represents the first light-weight overlay network called Arigatoni 1 that is suitable to deploy, via the Internet the Global Computing Communication Paradigm, i.e., computation via a...
Abstract ITRS 2004 Preliminary Version Towards an Intersection Typed System à la Church (2008)
Luigi Liquori, Inria Sophia Antipolis
In this paper, we presents a comfortable fully typed lambda calculus based on the well-known intersection type system discipline where proof are not only feasible but easy; the present system is the...
Alberto Ciaffaglione, Luigi Liquori, Marino Miculan
Abstract. We illustrate a methodology for formalizing and reasoning about Abadi and Cardelli’s object-based calculi, in (co)inductive type theory, such as the Calculus of (Co)Inductive...
Extending FeatherTrait Java with Interfaces (2008)
Liquori, Luigi, Spiwack, Arnaud
In the context of Featherweight Java by Igarashi, Pierce, and Wadler, and its recent extension FeatherTrait Java (FTJ) by the authors, we investigate classes that can be extended with trait...
FeatherTrait: A Modest Extension of Featherweight Java (2008)
Liquori, Luigi, Spiwack, Arnaud
In the context of statically-typed, class-based languages, we investigate classes that can be extended with trait composition. A trait is a collection of methods without state; it can be viewed as an...
Extending FeatherTrait Java with Interfaces (2008)
Liquori, Luigi, Spiwack, Arnaud
In the context of Featherweight Java by Igarashi, Pierce, and Wadler, and its recent extension FeatherTrait Java (FTJ) by the authors, we investigate classes that can be extended with trait...
FeatherTrait: A Modest Extension of Featherweight Java (2008)
Liquori, Luigi, Spiwack, Arnaud
In the context of statically-typed, class-based languages, we investigate classes that can be extended with trait composition. A trait is a collection of methods without state; it can be viewed as an...
Horatiu Cirstea, Claude Kirchner, Luigi Liquori
Abstract. The rewriting calculus, or Rho Calculus (Cal), is a simple calculus that uniformly integrates abstraction on patterns and nondeterminism. Therefore, it fully integrates rewriting and...
IOS Press A Subtyping for Extensible, Incomplete Objects To Helena Rasiowa: in memoriam (2007)
Viviana Bono, Michele Bugliesi, Mariangiola Dezani-ciancaglini, Luigi Liquori
Abstract. We extend the type system for the Lambda Calculus of Objects [16] with a mechanism of width subtyping and a treatment of incomplete objects. The main novelties over previous work are the...
A Typed Lambda Calculus of Objects (2007)
) Luigi Liquori 1 and Giuseppe Castagna 2 1 Dipartimento d'Informatica, Universit a di Torino C.so Svizzera 185, 10149 Torino, Italy 2 CNRS, LIENS-DMI, Ecole Normale Sup erieure, 45 rue...
Steffen Van, Luigi Liquori, Pawel Urzyczyn, Afdeling Informatica, Instytut Informatyki
We study the cube of type assignment systems, as introduced in [10]. This cube is obtained from Barendregt's typed -cube [1] via a natural type erasing function E, that erases type information...
Curriculum-vitae D, Concours Mdc, Luigi Liquori, L. Liquori, L. Liquori
Syntax Notation. Define the langage of data-types. 5 Common Management Information Protocol. 6 Telecommunication Management Network. Is a concept relative to nets and Telecommunication management. 7...
Alberto Ciaffaglione, Alberto Ciaffaglione, Luigi Liquori, Luigi Liquori, Marino Miculan, Marino Miculan, ...
apport de recherche
1.1 Sistemi di Assegnazione di Tipi per il-calcolo: : : : : : : : : : : : : : : 5 1.2 Sistemi Tipati per il-calcolo: : : : : : : : : : : : : : : : : : : : : : : : 7
Dealing with Explicit Exceptions in Prolog (2007)
Luigi Liquori, Maria Luisa Sapino
Existing logic languages provide some simple "extra-logical " constructs for control manipulation, such as the cut of standard Prolog and the exception handling constructs of other...
Universite Henry Poincare and Ecole des Mines de Nancy (2007)
Dominique Colnet, Luigi Liquori
It is well known that the Eiel language allows covariant redenition. Regardless of system-level validity rules, Eiel is not type safe. In this paper, we present a dialect of Eiel called Match-O,...
s, is a proper extension of (2007)
a conservative extension, called Ob 1, of the first-order Object Calculus Ob1 of Abadi and Cardelli, supporting method extension in presence of object subsumption. In this paper, we extend that work...
A Typed Lambda Calculus of Objects (Extended Abstract) (2007)
Abstract. In this paper, we present an explicitly typed version of the Lambda Calculus of Objects of [7], which is a development of the object-calculi defined in [10, 2]. This calculus supports...
Steffen Van Bakel, Luigi Liquori, Instytut Informatyki
We study the cube of type assignment systems, as introduced in [13], and confront it with Barendregt's typed-cube [4]. The first is obtained from the latter through applying a natural type...
Luigi Liquori, Pawe L Urzyczyn, Afdeling Informatica, Instytut Informatyki
We study the cube of type assignment systems, as introduced in [10]. This cube is obtained from Barendregt's typed -cube [1] via a natural type erasing function E, that erases type information...
calculus, a direct extension of the and the calculi. The main (2007)
Abstract. We develop a calculus which is a \direct " descendant of the blue calculus of Boudol [Bou97]. This calculus is both an extension of Abadi & Cardelli's &-calculus...
IOS Press A Subtyping for Extensible, Incomplete Objects To Helena Rasiowa: in memoriam (2007)
Viviana Bono, Michele Bugliesi, Mariangiola Dezani-ciancaglini, Luigi Liquori
Abstract. We extend the type system for the Lambda Calculus of Objects [16] with a mechanism of width subtyping and a treatment of incomplete objects. The main novelties over previous work are the...
Personal Address 37, rue du Lieutenant Crepin
Bounded Polymorphism for Extensible Objects (2007)
Ecole Normale, Superieure Lyon, Unite Mixte, Luigi Liquori, Luigi Liquori
In the ECOOP'97 conference, the author of the present paper investigated a conservative extension, called Ob 1, of the first-order Object Calculus Ob 1 of Abadi and Cardelli, supporting method...
Certified Reasoning on Real Numbers and Objects in Co-inductive Type Theory Candidate: (2007)
École Nationale, Supérieure Mines, Furio Honsell, Pietro Di Gianantonio, Claude Kirchner, Luigi Liquori, ...
In this thesis we adopt Formal Methods based on Type Theory for reasoning on the semantics of computer programs. The ultimate goal is their certification, that is, to prove that a fragment of...
Foundations for dynamic object re-classification (2007)
Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell, Luigi Liquori
We investigate, in the context of functional prototype-based languages, objects which might extend themselves upon receiving a message. The possibility for an object of extending its own...
Abstract. We propose and discuss foundations for programmable overlay networks and overlay computing systems. Such overlays are built over a large number of distributed computational individuals,...
Abstract. We propose and discuss foundations for programmable overlay networks and overlay computing systems. Such overlays are built over a large number of distributed computational individuals,...
Resource Discovery in the Arigatoni Model. (2006)
Chand, Raphael, Liquori, Luigi, Cosnard, Michel
Arigatoni is a lightweight communication model for dynamic Resource Discovery. Inspired by the Publish/Subscribe paradigm, the Arigatoni model implements a Resource-Discovery Oriented Overlay...
Resource Discovery in the Arigatoni Model. (2006)
Chand, Raphael, Liquori, Luigi, Cosnard, Michel
Arigatoni is a lightweight communication model for dynamic Resource Discovery. Inspired by the Publish/Subscribe paradigm, the Arigatoni model implements a Resource-Discovery Oriented Overlay...
Resource Discovery in the Arigatoni Model. (2006)
Chand, Raphael, Liquori, Luigi, Cosnard, Michel
Arigatoni is a lightweight communication model for dynamic Resource Discovery. Inspired by the Publish/Subscribe paradigm, the Arigatoni model implements a Resource-Discovery Oriented Overlay...
Arigatoni>: Overlaying Internet via Low Level Network Protocols (2006)
Benza, Didier, Cosnard, Michel, Liquori, Luigi, Vesin, Marc
We design a lightweight communication model, called Arigatoni, with related architecture, that is suitable to deploy the Global Computing Paradig} over the Internet. Communication over the behavioral...
Decidable Type Inference for the Polymorphic Rewriting Calculus (2006)
Cirstea, Horatiu, Kirchner, Claude, Liquori, Luigi, Wack, Benjamin
The rewriting calculus is a minimal framework embedding lambda calculus and term rewriting systems that allows abstraction on variables and patterns. The rewriting calculus features higher-order...
Arigatoni: Overlaying Internet via Low Level Network Protocols (2006)
Benza, Didier, Cosnard, Michel, Liquori, Luigi, Vesin, Marc
We design a lightweight communication model, called Arigatoni, with related architecture, that is suitable to deploy the Global Computing Paradig} over the Internet. Communication over the behavioral...
Resource Discovery in the Arigatoni Model. (2006)
Chand, Raphael, Liquori, Luigi, Cosnard, Michel
Arigatoni is a lightweight communication model for dynamic Resource Discovery. Inspired by the Publish/Subscribe paradigm, the Arigatoni model implements a Resource-Discovery Oriented Overlay...
A Framework for Defining Logical Frameworks (2006)
Liquori, Luigi, Honsell, Furio, Lenisa, Marina
In this paper, we introduce a General Logical Framework, called GLF, for defining Logical Frameworks, based on dependent types, in the style of the well known Edinburgh Logical Framework LF. The...
A Framework for Defining Logical Frameworks (2006)
Liquori, Luigi, Honsell, Furio, Lenisa, Marina
In this paper, we introduce a General Logical Framework, called GLF, for defining Logical Frameworks, based on dependent types, in the style of the well known Edinburgh Logical Framework LF. The...
A Framework for Defining Logical Frameworks (2006)
Liquori, Luigi, Honsell, Furio, Lenisa, Marina
In this paper, we introduce a General Logical Framework, called GLF, for defining Logical Frameworks, based on dependent types, in the style of the well known Edinburgh Logical Framework LF. The...
A Framework for Defining Logical Frameworks (2006)
Liquori, Luigi, Honsell, Furio, Lenisa, Marina
In this paper, we introduce a General Logical Framework, called GLF, for defining Logical Frameworks, based on dependent types, in the style of the well known Edinburgh Logical Framework LF. The...
Resource Discovery in the Arigatoni Model. (2006)
Chand, Raphael, Liquori, Luigi, Cosnard, Michel
Arigatoni is a lightweight communication model for dynamic Resource Discovery. Inspired by the Publish/Subscribe paradigm, the Arigatoni model implements a Resource-Discovery Oriented Overlay...
Arigatoni: Overlaying Internet via Low Level Network Protocols (2006)
Benza, Didier, Cosnard, Michel, Liquori, Luigi, Vesin, Marc
We design a lightweight communication model, called Arigatoni, with related architecture, that is suitable to deploy the Global Computing Paradig} over the Internet. Communication over the behavioral...
A Framework for Defining Logical Frameworks (2006)
Liquori, Luigi, Honsell, Furio, Lenisa, Marina
In this paper, we introduce a General Logical Framework, called GLF, for defining Logical Frameworks, based on dependent types, in the style of the well known Edinburgh Logical Framework LF. The...
Decidable Type Inference for the Polymorphic Rewriting Calculus (2006)
Cirstea, Horatiu, Kirchner, Claude, Liquori, Luigi, Wack, Benjamin
The rewriting calculus is a minimal framework embedding lambda calculus and term rewriting systems that allows abstraction on variables and patterns. The rewriting calculus features higher-order...
Luigi Liquori, Bernard Paul Serpette
We propose an imperative version of the Rewriting-calculus, a calculus based on pattern-matching, pattern-abstraction, and side-effects, which we call iRho. We formulate a static and a big-step...
1.1. Addressed Calculi and Semantics of Sharing (2006)
Daniel J. Dougherty, Pierre Lescanne, Luigi Liquori
We present a formalism called Addressed Term Rewriting Systems, which can be used to model implementations of theorem proving, symbolic computation, and programming languages, especially aspects of...
A framework for defining logical frameworks (2006)
Thème Sym, Furio Honsell, Furio Honsell, Marina Lenisa, Marina Lenisa, Luigi Liquori, ...
apport de recherche SN 0249-6399 ISRN INRIA/RR--????--FR+ENG
Decidable Type Inference for the Polymorphic Rewriting Calculus (2005)
Cirstea, Horatiu, Kirchner, Claude, Liquori, Luigi, Wack, Benjamin
The rewriting calculus is a minimal framework embedding lambda calculus and term rewriting systems that allows abstraction on variables and patterns. The rewriting calculus features higher-order...
Types for REWERSE reasoning and query languages (2005)
Cirstea, Horatiu, Coquery, Emmanuel, Drabent, Wlodzimierz, Fages, François, Kirchner, Claude, Liquori, Luigi, ...
This report presents proposals for a type system for a subset of REWERSE languages. We study two approaches to such a type system, which are based on descriptive and prescriptive typing. As an...
Types for REWERSE reasoning and query languages (2005)
Cirstea, Horatiu, Coquery, Emmanuel, Drabent, Wlodzimierz, Fages, François, Kirchner, Claude, Liquori, Luigi, ...
This report presents proposals for a type system for a subset of REWERSE languages. We study two approaches to such a type system, which are based on descriptive and prescriptive typing. As an...
Featherweight-Trait Java : A Trait-based Extension for FJ (2004)
Liquori, Luigi, Spiwack, Arnaud
In the context of statically typed class-based languages, we investigate classes which might extend upon trait composition. Building classes by composing method-clusters is a well-known technique in...
Featherweight-Trait Java : A Trait-based Extension for FJ (2004)
Liquori, Luigi, Spiwack, Arnaud
In the context of statically typed class-based languages, we investigate classes which might extend upon trait composition. Building classes by composing method-clusters is a well-known technique in...
Featherweight-Trait Java : A Trait-based Extension for FJ (2004)
Liquori, Luigi, Spiwack, Arnaud
In the context of statically typed class-based languages, we investigate classes which might extend upon trait composition. Building classes by composing method-clusters is a well-known technique in...
On the Formalization of Imperative Object-based Calculiin (Co)Inductive Type Theories (2003)
Ciaffaglione, Alberto, Liquori, Luigi, Miculan, Marino
In this paper, we study the formalization of Abadi and Cardelli's , a representative object-based calculus with types and side effects, in interactive proof assistants based on (Co)Inductive Type...
On the Formalization of Imperative Object-based Calculiin (Co)Inductive Type Theories (2003)
Ciaffaglione, Alberto, Liquori, Luigi, Miculan, Marino
In this paper, we study the formalization of Abadi and Cardelli's , a representative object-based calculus with types and side effects, in interactive proof assistants based on (Co)Inductive Type...
On the Formalization of Imperative Object-based Calculiin (Co)Inductive Type Theories (2003)
Ciaffaglione, Alberto, Liquori, Luigi, Miculan, Marino
In this paper, we study the formalization of Abadi and Cardelli's , a representative object-based calculus with types and side effects, in interactive proof assistants based on (Co)Inductive Type...
Rewriting calculus with fixpoints: Untyped and first-order systems (2003)
Horatiu Cirstea, Luigi Liquori, Benjamin Wack, Nancy Ii, Nancy I
Abstract The rewriting calculus, also called ρ-calculus, is a framework embedding λ-calculus and rewriting capabilities, by allowing abstraction not only on variables but also on patterns. The...
On the formalization of imperative object-based calculi in (co)inductive type theories (2003)
Alberto Ciaffaglione, Luigi Liquori, Marino Miculan
Abstract. We discuss the formalization of Abadi and Cardelli’s impς, a paradigmatic object-based calculus with types and side effects, in (Co)Inductive Type Theories. Instead of representing...
Imperative Object-based Calculi in (Co)Inductive Type Theories (2003)
Alberto Ciaffaglione, Luigi Liquori, Marino Miculan
Abstract. We discuss the formalization of Abadi and Cardelli’s impς, a paradigmatic object-based calculus with types and side effects, in Co-Inductive Type Theories, such as the Calculus of...
A Generic Object-Calculus Based onAddressed Term Rewriting Systems (2002)
Dougherty, Dan, Lang, Frédéric, Lescanne, Pierre, Liquori, Luigi, Rose, Kristoffer
We describe the foundations of , a framework, or generic calculus, for modeling object-oriented programming languages. This framework provides a setting for a formal operational semantics of object...
A Generic Object-Calculus Based on Addressed Term Rewriting Systems (2002)
Dougherty, Dan, Lang, Frédéric, Lescanne, Pierre, Liquori, Luigi, Rose, Kristoffer
We describe the foundations of , a framework, or generic calculus, for modeling object-oriented programming languages. This framework provides a setting for a formal operational semantics of object...
A Generic Object-Calculus Based on Addressed Term Rewriting Systems (2002)
Dougherty, Dan, Lang, Frédéric, Lescanne, Pierre, Liquori, Luigi, Rose, Kristoffer
We describe the foundations of , a framework, or generic calculus, for modeling object-oriented programming languages. This framework provides a setting for a formal operational semantics of object...
Rewriting calculus with(out) types (2002)
Horatiu Cirstea, Claude Kirchner, Luigi Liquori
The last few years have seen the development of a new calculus which can be considered as an outcome of the last decade of various researches on (higher order) term rewriting systems, and lambda...
A Generic Object-Calculus Based on Addressed Term Rewriting Systems (2002)
Dan Dougherty, Pierre Lescanne, Luigi Liquori
We describe the foundations of Obj +a, a framework, or generic calculus, for modeling object-calculi. This framework is essentially a detailed formal operational semantics of object based languages,...
Horatiu Cirstea, Claude Kirchner, Luigi Liquori
www.loria.fr/{~cirstea,~ckirchne,~lliquori} Abstract. The rewriting calculus, or Rho Calculus (ρCal), is a simple calculus that uniformly integrates abstraction on patterns and nondeterminism....
Horatiu Cirstea, Claude Kirchner, Luigi Liquori
www.loria.fr/f~cirstea,~ckirchne,~lliquorig Abstract. The rewriting calculus, or Rho Calculus (Cal), is a simple calculus that uniformly integrates abstraction on patterns and nondeterminism....
Horatiu Cirstea, Claude Kirchner, Luigi Liquori
www.loria.fr/{˜cirstea,˜ckirchne,˜lliquori} Abstract. In this paper we give a simple and uniform presentation of the rewriting calculus, also called Rho Calculus. In addition to its simplicity,...
A generic object-calculus based on Addressed Term Rewriting Systems. (1999)
Dougherty, Daniel, Lang, Frédéric, Lescanne, Pierre, Liquori, Luigi, Rose, Kristoffer
(eng) In a previous paper we have outlined a framework (or a generic object-calculus) called \Obja, for modeling \textit{object calculi}. In this one, we would like to describe the foundations of...
A Framework for Defining Object-Calculi (Extended Abstract (1999)
Frederic Lang, Pierre Lescanne, Luigi Liquori
Abstract. In this paper, we give a general framework for the foundation of an operational (small step) semantics of object-based languages with an emphasis on functional and imperative issues. The...
A Generic Object-Calculus Based on Addressed Term Rewriting Systems (1999)
Pierre Lescanne, Frédéric Lang, Daniel Dougherty, Daniel Dougherty, Kristoffer Rose, Luigi Liquori, ...
In a previous paper we have outlined a framework (or a generic object-calculus) called Obj +a , for modeling object calculi. In this one, we would like to describe the foundations of Obj +a . This...
A Framework for Defining Object-Calculi. (1998)
Lang, Frédéric, Lescanne, Pierre, Liquori, Luigi
(eng) In this paper, we give a general framework for the foundation of an operational (small step) semantics of object-based languages with an emphasis on functional and imperative issues. The...
Abstract. The last few years have seen the development of statically typed object based (also called prototype-based) programming languages. Two proposals, namelythe Lambda Calculus of Objects of...
Abstract. The last few years have seen the development of statically typed object based (also called prototype-based) programming languages. Two proposals, namely the Lambda Calculus of Objects of...
A Lambda Calculus of Objects with Self-in Extension (1998)
Pietro Di Gianantonio, Furio Honsell, Luigi Liquori
In this paper we investigate, in the context of functional prototype-based languages, objects which might extend themselves upon receiving a message. The possibility for an object of extending its...
A Framework for Defining Object-Calculi (Extended Abstract) (1998)
Frédéric Lang, Ecole Normale, Superieure Lyon, Unite Mixte, Pierre Lescanne, ...
Frederic Lang Pierre Lescanne Luigi Liquori Decembre 1998 Research Report N o RR 1998-51 Ecole Normale Sup erieure de Lyon 46 Allee d'Italie, 69364 Lyon Cedex 07, France Telephone :...
A Subtyping for Extensible, Incomplete Objects (1998)
Viviana Bono, Michele Bugliesi, Mariangiola Dezani-ciancaglini, Luigi Liquori
We extend the type system for the Lambda Calculus of Objects [16] with a mechanism of width subtyping and a treatment of incomplete objects. The main novelties over previous work are the use of...
A Lambda Calculus of Objects with Self-Inflicted Extension (1998)
Pietro Di Gianantonio, Furio Honsell, Luigi Liquori
In this paper we investigate, in the context of functional prototype-based languages, objects which might extend themselves upon receiving a message. The possibility for an object of extending its...
Comparing cubes of typed and type assignment systems (1997)
Steffen Van Bakel, Luigi Liquori, Paweł Urzyczyn
We study the cube of type assignment systems, as introduced in [13], and confront it with Barendregt’s typed λ-cube [4]. The first is obtained from the latter through applying a natural type...
Subtyping Constraints for Incomplete Objects (1997)
Viviana Bono, Michele Bugliesi, Luigi Liquori
Abstract. We extend the type system for the Lambda Calculus of Objects [14] to account for a notion of width subtyping. The main novelties over previous work are the use of bounded quantication to...
An Extended Theory of Primitive Objects: First Order System (1997)
Abstract. We investigate a first-order extension of the Theory of Primitive Objects of [5] that supports method extension in presence of object subsumption. Extension is the ability of modifying the...
Comparing Cubes of Typed and Type Assignment Systems (1997)
Steffen Van Bakel, Luigi Liquori, Pawel Urzyczyn
We study the cube of type assignment systems, as introduced in [13], and confront it with Barendregt's typed -cube [4]. The first is obtained from the latter through applying a natural type...
A Lambda Calculus of Incomplete Objects (1996)
Viviana Bono, Michele Bugliesi, Luigi Liquori
Abstract. This paper extends the Lambda Calculus of Objects as proposed in [5] with a new support for incomplete objects. Incomplete objects behave operationally as “standard ” objects; their...
A Lambda Calculus of Incomplete Objects (1996)
Viviana Bono, Michele Bugliesi, Luigi Liquori
Abstract. This paper extends the Lambda Calculus of Objects as proposed in [5] with a new support for incomplete objects. Incomplete objects behave operationally as \standard " objects;...
A linear logic calculus of objects (1996)
Michele Bugliesi, Giorgio Delzanno, Luigi Liquori, Maurizio Martelli
This paper presents a linear logic programming language, called O \Gammaffi, that gives a complete account of an object-oriented calculus with inheritance and override. This language is best...
A Lambda Calculus of Incomplete Objects (1996)
Viviana Bono, Michele Bugliesi, Luigi Liquori
This paper extends the Lambda Calculus of Objects as proposed in [5] with a new support for incomplete objects. Incomplete objects behave operationally as \standard" objects; their typing,...
A Subtyping for the Fisher-Honsell-Mitchell (1995)
Lambda Calculus Of, Viviana Bono, Luigi Liquori
Labeled types and a new relation between types are added to the lambda calculus of objects as described in [5]. This relation is a trade-off between the possibility of having a restricted form of...
Steffen Van Bakel, Luigi Liquori, Pawel Urzyczyn, Afdeling Informatica, Instytut Informatyki
We study the cube of type assignment systems, as introduced in [10]. This cube is obtained from Barendregt's typed -cube [1] via a natural type erasing function E, that erases type information...