An Intuitive Automated Modelling Interface for Systems Biology (2009)
Kahramanoğullari, Ozan, Cardelli, Luca, Caron, Emmanuelle
We introduce a natural language interface for building stochastic pi calculus models of biological systems. In this language, complex constructs describing biochemical events are built from basic...
From X to π; representing the classical sequent calculus (2009)
Steffen Van Bakel, Luca Cardelli, Maria Grazia Vigliotti
Abstract. We study the π-calculus, enriched with pairing and non-blocking input, and define a notion of type assignment that uses the type constructor →. We encode the circuits of the calculus X...
FBTC 2008 A Process Model of Actin Polymerisation (2009)
Luca Cardelli, Emmanuelle Caron, Andrew Phillips
Actin is the monomeric subunit of actin filaments which form one of the three major cytoskeletal networks in eukaryotic cells. Actin dynamics, be it the polymerisation of actin monomers into...
AN INTUITIVE AUTOMATED MODELLING INTERFACE FOR SYSTEMS BIOLOGY (2009)
Ozan Kahramanoğulları, Luca Cardelli, Emmanuelle Caron
Modelling of biological systems by mathematical and computational techniques is becoming increasingly widespread in research on biological systems. However, expressing biological knowledge in...
A PROCESS MODEL OF ACTIN POLYMERISATION (2009)
Luca Cardelli, Emmanuelle Caron, Ozan Kahramanoğulları, Andrew Phillips
Actin is the monomeric subunit of actin filaments which form one of the three major cytoskeletal networks in eukaryotic cells. Actin dynamics, be it the polymerisation of actin monomers into...
A Process Model of Rho GTP-binding Proteins (2009)
Luca Cardelli, Emmanuelle Caron, Andrew Phillips
Rho GTP-binding proteins play a key role as molecular switches in many cellular activities. In response to extracellular stimuli and with the help from regulators (GEF, GAP, Effector, GDI), these...
Abstract:Object-oriented languages dominate procedural languages in certain software-engineering categories but not in others. Further progress may involve adapting and reintroducing principles that...
A Process Model of Rho GTP-binding Proteins (2008)
Luca Cardelli, Emmanuelle Caron, Andrew Phillips
Rho GTP-binding proteins play a key role as molecular switches in many cellular activities. In response to extracellular stimuli and with the help from regulators (GEF, GAP, Effector, GDI), these...
Preface Can a Systems Biologist (2008)
Fix A Tamagotchi, Luca Cardelli
Gilles Kahn was a serious scientist, but part of his style and effectiveness was in the great sense of curiosity and fun that he injected in the most technical topics. Some of his later projects...
● From Processes to ODEs (2008)
Luca Cardelli, Two Stochastics, Mhc Class, I Flytrap, Groupies Ode, Luca Cardelli
Leibniz, Discourse de métaphysique. Paraphrased by G.Chaitin.
Cristiano Calcagno, Luca Cardelli, Andrew D. Gordon
We consider a propositional spatial logic for finite trees. The logic includes A | B (tree composition), A ⊲ B (the implication induced by composition), and 0 (the unit of composition). We show...
RÉPARTIE ET MOBILE The Join-Calculus: a Calculus for Distributed Mobile Programming (2008)
Docteur De, Cédric Fournet, Mm. Robin, Milner Président, Gérard Boudol, ...
présentée à
Cristiano Calcagno, Luca Cardelli, Andrew D. Gordon
We consider a propositional spatial logic for finite trees. The logic includes A | B (tree composition), A ⊲ B (the implication induced by composition), and 0 (the unit of composition). We show...
Reactions vs. Components (2008)
Andrew Phillips, Luca Cardelli, Individual Reactions
Map out the complete genetic code in humans To understand and predict gene and protein behaviour Like reading the source code of a computer program... But functional meaning of the code is still a...
A Pure Calculus of Subtyping, and Applications (Outline) (2008)
One of the problems in understanding object-oriented languages is understanding their type systems, e.g. making sure that they are sound. To this end, I propose a typed foundation for object-oriented...
A Process Model of Rho GTP-binding Proteins in the Context of Phagocytosis (2008)
At the early stages of the phagocytic signalling, Rho GTP-binding proteins play a key role. With the stimulus from the cell membrane and with the help from the regulators (GEF, GAP, Effector, GDI),...
Towards Systems Biology (2008)
Luca Cardelli, Ralf Blossey, Andrew Phillips
different nucleotides – Direct protein assembly through RNA and the Genetic Code ● Proteins (>10000) are made of amino acids – Process signals – Activate genes – Move materials –...
Abstract Machines of Systems Biology (Extended Abstract) (2008)
Summary. Living cells are extremely well-organized autonomous systems, consisting of discrete interacting components. Key to understanding and modelling their behavior is modelling their system...
1 Introduction Type Systems (2008)
The fundamental purpose of a type system is to prevent the occurrence of execution errors during
Where Membranes Meet Complexes (2008)
Luca Cardelli, Sylvain Pradalier
We introduce a calculus handling complexation of molecules and membranes. The approach is based on adding dynamic interfaces to processes, which induce bonds between molecules. The calculus is then...
In: "Combinators and Functional Programming Languages" (2008)
The Amber machine is a stack machine designed as an intermediate language for compiling higher-order languages. The current version is specialized for the Amber language. The machine supports a set...
Abstract Bitonal Membrane Systems Interactions of Biological Membranes (2008)
Inspired by the alternating orientations of cellular membranes, we describe a structure of nested membranes that are colored in two alternating tones. We investigate a class of reactions that...
Bad Engineering Properties of Object-Oriented Languages (2008)
Object-oriented languages dominate procedural languages in certain software-engineering categories, but not in others. Further progress may involve adapting and reintroducing principles that are...
Ac Martín Abadi, Luca Cardelli, A Theory, Objects Springer, ...
[Ble79] Woodrow W. Bledsoe. A maximal method for set variables. Machine
1 Introduction Semistructured Computation (2008)
This paper is based on the observation that the areas of semistructured databases [1]
Towards Systems Biology (2008)
different nucleotides – Direct protein assembly through RNA and the Genetic Code ● Proteins (>10000) are made of amino acids – Process signals – Activate genes – Move materials –...
Abstract Secrecy and Group Creation (2008)
Luca Cardelli, Giorgio Ghelli, Andrew D. Gordon
We add an operation of group creation to the typed π-calculus, where a group is a type for channels. Creation of fresh groups has the effect of statically preventing certain communications, and can...
Appears in Seminar on Concurrency (2008)
This paper describes the low-level primitives necessary to implement a particular flavor or inter-process communication. It is motivated by the design of a communication subsystem for a higher-order...
Journal of Functional Programming, 1(4):375–416, 1991a. Summary in (2008)
Anindya Banerjee, Nevin Heintze, Luca Cardelli, Luca Cardelli, Benjamin Pierce
Abadi, Martín and Luca Cardelli. On subtyping and matching. In European Conference
OOPSLA'96 Tutorial August 12, 1996 4:12 pm 1 (2007)
Theory Of Objects, Luca Cardelli, Kernel Properties
0> 0 (code for get) (code for set) object reference attribute record Class-Based Languages August 12, 1996 4:44 pm 7 Object Operations Object creation. ~ InstanceTypeOf(c) indicates the type of an...
Berkeley `97 March 6, 1997 1:57 pm 1 (2007)
Luca Cardelli, Objecttype Cell
method set ( n : Integer ) is self . contents := n end ; end ; Object-Based Languages March 9, 1997 10:43 pm 5 An Object Generator Procedures as object generators. Quite similar to classes! procedure...
Distributed Mobile Computation in Obliq (2007)
Obliq is lexically-scoped, untyped, interpreted language that supports distributed object -oriented computation. Obliq objects have state and are local to a site. Obliq computations can roam over the...
type: A data type whose nature is kept hidden, in such a way that only a predetermined collection of operations can operate on it. Contravariant: A type that varies in the inverse direction from one...
A Theory of Primitive Objects (2007)
Untyped And First-Order, Martín Abadi, Luca Cardelli
We introduce simple object calculi that support method override and object subsumption. We give an untyped calculus, typing rules, and equational rules. We illustrate the expressiveness of our...
PLDI'96 Tutorial April 30, 1996 12:20 pm 1 (2007)
Class-based object-oriented programming languages take object generators as central, while object-based languages emphasize the objects themselves. This dichotomy, or spectrum, has been explicitly...
PLDI'96 Tutorial April 30, 1996 12:20 pm 1 (2007)
Luca Cardelli, Luca Cardelli, Kernel Properties
Class-based object-oriented programming languages take object generators as central, while object-based languages emphasize the objects themselves. This dichotomy, or spectrum, has been explicitly...
Mobile Ambients (Extended Abstract) (2007)
Luca Cardelli, Mobile Ambients, Andrew D. Gordon
There are two distinct areas of work in mobility: mobile computing, concerning computation that is carried out in mobile devices (laptops, personal digital assistants, etc.), and mobile computation,...
An implementation of F<: (2007)
F<: is a highly expressive typed #-calculus with subtyping. This paper describes an implementation of F<: (extended with recursive types), and documents the algorithms used. Using this...
ATT Bell Laboratories Murray Hill, New Jersey 07974 (2007)
This paper describes the low-level primitives necessary to implement a particular flavor or inter-process communication. It is motivated by the design of a communication subsystem for a higher-order...
Département de Mathématiques et Informatique (2007)
Uperieure Ormale, N Ecole, Kim B. Bruce, Kim B. Bruce, Luca Cardelli, Luca Cardelli, ...
Giving types to binary methods causes significant problems for object-oriented language designers and programmers. This paper offers a comprehensive description of the problems arising from typing...
ATT Bell Laboratories, Murray Hill, NJ 07974 (2007)
Introduction The Amber language embeds many recent ideas in programming language design, and tries to introduce all the features in their minimal, essential, form. One of its main goals is to safely...
F<: is a highly expressive typed #-calculus with subtyping. This paper describes an implementation of F<: (extended with recursive types), and documents the algorithms used. Using this...
Luca Cardelli, Giorgio Ghelli, Andrew D. Gordon
Abstract. We add an operation of group creation to the typed-calculus, where a group is a type for channels. Creation of fresh groups has the effect of statically preventing certain communications,...
G.: Querying trees with pointers (2007)
We introduce a data model for semi-structured data and explore a spatial logic for reasoning about this model. This note is part of an on-going project to develop a pattern-matching language for...
Microsoft Research, Cambridge. Deciding Validity in a Spatial Logic for Trees (2007)
Cristiano Calcagno, Cristiano Calcagno, Luca Cardelli, Luca Cardelli, Andrew D. Gordon, Andrew D. Gordon
We consider a propositional spatial logic for finite trees. The logic includes A | B (tree composition), A ⊲ B (the implication induced by composition), and 0 (the unit of composition). We show...
Roger Needham, Roger Needham, Martín Abadi, Ross Anderson, Jean Bacon, Andrew Birrell, ...
comprising in this compilation are copyright of the respective authors. All rights are reserved. This publication may not be copied, reproduced, published or distributed in whole or in part in any...
Abstract. The ambient logic is a modal logic proposed to describe the structural and computational properties of distributed and mobile computation. The structural part of the ambient logic is,...
Obliq is a lexically-scoped untyped language that supports distributed object-oriented computation. An Obliq computation may involve multiple threads of control within an address space, multiple...
Obliq is a lexically-scoped untyped interpreted language that supports distributed object-oriented computation. An Obliq computation may involve multiple threads of control within an address space,...
Luca Cardelli, Giorgio Ghelli, Andrew D. Gordon
The ambient calculus is a concurrent calculus where the unifying notion of `ambient ' is used to model many dierent constructs for distributed and mobile computation. We study a type system that...
Luca Cardelli, Luca Cardelli, Rowan Davies, Rowan Davies
work may not be copied or reproduced in whole or in part for any commercial purpose.
Andrew D. Gordon, Luca Cardelli
The ambient calculus is a process calculus for describing mobile computation. We develop a theory of Morris-style contextual equivalence for proving properties of mobile ambients. We prove a context...
0 = Rx: Ry: (S! R): x: S succ = n: S Rx: Ry: (S! R): yn: S! S (2007)
In the untyped lambda calculus, the Scott numerals are defined by: 0 = xy: x succ = nxy: yn case = naf: naf where case(n)(a)(f) returns a if n is 0 and f(x) if n is the successor of x (see, e.g.,...
Nick Benton, Luca Cardelli, Polyphonic C
is an extension of the C language with new asynchronous concurrency constructs, based on the Join Calculus. We describe the design and implementation of the language and give examples of its use in...
Quest is a programming language based on impredicative type quantifiers and subtyping within a three-level structure of kinds, types and type operators, and values. The semantics of Quest is rather...
Luca Cardelli, Simone Martini, John C. Mitchell, Andre Scedrov
System F is a well-known typed l-calculus with polymorphic types, which provides a basis for polymorphic programming languages. We study an extension of F, called F (pronounced ef-sub) that combines...
Lecture Notes in Computer Science 197 (2007)
An implementation model of rendezvous communication
The Amber machine is a stack machine designed as an intermediate language for compiling higher-order languages. The current version is specialized for the Amber language. The machine supports a set...
By the term data-oriented language, I mean a language whose main concern is in the structuring and handling of data. For contrast, procedure-oriented and process-oriented languages are mostly...
Nick Benton, Luca Cardelli, Cédric Fournet
Polyphonic C ♯ is an extension of the C ♯ language with new asynchronous concurrency constructs, based on the join calculus. We describe the design and implementation of the language and give...
And Rowan Davies, Luca Cardelli, Luca Cardelli, Rowan Davies, Rowan Davies
The World-Wide Web is rich in content and services, but access to these resources must be obtained mostly through manual browsers. Wewould like to be able to write programs that reproduce human...
Efficient, correct simulation of biological processes in the stochastic pi-calculus (2007)
Andrew Phillips, Luca Cardelli
Abstract. This paper presents a simulation algorithm for the stochastic π-calculus, designed for the efficient simulation of biological systems with large numbers of molecules. The cost of a...
in dynamic models of gene regulation (2007)
Ralf Blossey, Ralf Blossey, Luca Cardelli, Andrew Phillips
We present an approach for constructing dynamic models for the simulation of gene regulatory networks from simple computational elements. Each element is called a “gene gate ” and defines an...
Efficient, correct simulation of biological processes in the stochastic pi-calculus (2007)
Andrew Phillips, Luca Cardelli
Abstract. This paper presents a simulation algorithm for the stochastic pi-calculus, designed for the efficient simulation of biological systems with large numbers of molecules. The cost of a...
A Compositional Approach to the Stochastic Dynamics of Gene Networks (2006)
Ralf Blossey, Luca Cardelli, Andrew Phillips
Abstract. We propose a compositional approach to the dynamics of gene regulatory networks based on the stochastic π-calculus, and develop a representation of gene network elements which can be used...
A Compositional Approach to the Stochastic Dynamics of Gene Networks (2006)
Ralf Blossey, Luca Cardelli, Andrew Phillips
Abstract. We propose a compositional approach to the dynamics of gene regulatory networks based on the stochastic π-calculus, and develop a representation of gene network elements which can be used...
A Graphical Representation for Biological Processes in the Stochastic pi-calculus (2006)
Andrew Phillips, Luca Cardelli
Abstract. This paper presents a graphical representation for the stochastic π-calculus, which is formalised by defining a corresponding graphical calculus. The graphical calculus is shown to be...
Abstract machines of systems biology (2005)
Abstract. Living cells are extremely well-organized autonomous systems, consisting of discrete interacting components. Key to understanding and modeling their behavior is modeling their system...
Brane Calculi. Interactions of Biological Membranes (2005)
Abstract. We introduce a family of process calculi with dynamic nested membranes. In contrast to related calculi, including some developed for biological applications, active entities here are...
Ac Martìn Abadi, Luca Cardelli, A Theory, Objects Springer, An Arvind
machine instructions for proof-carrying code. In 27th Symposium on the Principles of Programming Languages (POPL), pages 243–253,
Abstract machines of systems biology (2005)
Abstract. Living cells are extremely well-organized autonomous systems, consisting of discrete interacting components. Key to understanding and modeling their behavior is modeling their system...
A graphical representation for the stochastic pi-calculus (2005)
Andrew Phillips, Luca Cardelli
Abstract. This paper presents a graphical representation for the stochastic pi-calculus, which builds on previous formal and informal notations. The graphical representation is used to model a Mapk...
A graphical representation for the stochastic pi-calculus (2005)
Andrew Phillips, Luca Cardelli, Andrew Phillips Bioconcur
➢ Stochastic pi-calculus used to model and simulate a range of biological systems [Lecca and Priami, 2003, Priami et al., 2001, Regev et al., 2001]: ❑ Able to model independent system components,...
Luca Cardelli, Giovanni Conforti, Giorgio Ghelli, Silvano Dal-zilio
Spatial Logics have been recently proposed as modal logics inspecting the ‘spatial’ nature of models (as opposed to ‘temporal logics ’ inspecting model behavior). Spatial Logics, essentially,...
Ac Martìn Abadi, Luca Cardelli, A Theory, Objects Springer, An Arvind, ...
machine instructions for proof-carrying code. In 27th Symposium on the Principles of Programming Languages (POPL), pages 243–253,
Greedy regular expression matching (2004)
This paper studies the problem of matching sequences against regular expressions in order to produce structured values.
A correct abstract machine for the stochastic pi-calculus (2004)
Andrew Phillips, Luca Cardelli
Abstract. This paper presents an abstract machine for a variant of the stochastic pi-calculus, in order to correctly model the stochastic simulation of biological processes. The abstract machine is...
A correct abstract machine for the stochastic pi-calculus (2004)
Andrew Phillips, Luca Cardelli, Andrew Phillips Bioconcur
❑ Use process calculi to model biological systems ➢ Features of process calculi: ❑ Compositional modelling, analysis and simulation of systems. ➢ Potential Benefits:
A correct abstract machine for the stochastic pi-calculus (2004)
Andrew Phillips, Luca Cardelli
In this paper, an abstract machine is presented for a variant of the stochastic picalculus, in order to correctly model the stochastic simulation of biological processes. The machine is first proved...
Subtyping and Parametricity (2003)
Plotkin, Gordon, Abadi, Martin, Cardelli, Luca
In this paper we study the interaction of subtyping and parametricity. We describe a logic for a programming language with parametric polymorphism and subtyping. The logic supports the formal...
Subtyping and Parametricity (2003)
Plotkin, Gordon, Abadi, Martin, Cardelli, Luca
In this paper we study the interaction of subtyping and parametricity. We describe a logic for a program- ming language with parametric polymorphism and sub- typing. The logic supports the formal...
TQL: A query language for semistructured data based on the ambient logic (2003)
The ambient logic is a modal logic proposed to describe the structural and computational properties of distributed and mobile computation. The structural part of the ambient logic is, essentially, a...
Deciding validity in a spatial logic for trees (2003)
Cristiano Calcagno, Luca Cardelli, Andrew D. Gordon
Abstract. We consider a propositional spatial logic for finite trees. The logic includes A | B (spatial composition), and A ⊲ B (the implication induced by composition), and 0 (the unit of...
Distributed Mobile Computation in (2003)
Obliq is lexically-scoped, untyped, interpreted language that supports distributed object-oriented computation. Obliq objects have state and are local to a site. Obliq computations can roam over the...
Modern Concurrency Abstractions for C (2002)
Nick Benton, Luca Cardelli, Polyphonic C
is an extension of the C language with new asynchronous concurrency constructs, based on the join calculus. We describe the design and implementation of the language and give examples of its use in...
A spatial logic for concurrency (part II (2002)
We present a modal logic for describing the spatial organization and the behavior of distributed systems. In addition to standard logical and temporal operators, our logic includes spatial operations...
A spatial logic for querying graphs (2002)
Abstract. We study a spatial logic for reasoning about labelled directed graphs, and the application of this logic to provide a query language for analysing and manipulating such graphs. We give a...
Deciding Validity in a Spatial Logic for Trees (2002)
Cristiano Calcagno Imperial, Cristiano Calcagno, Andrew D. Gordon, Luca Cardelli
We consider a propositional spatial logic for finite trees. The logic includes (tree composition), (the implication induced by composition) , and 0 (the unit of composition). We show that the...
Modern Concurrency Abstractions for C (2002)
Nick Benton, Luca Cardelli, Cédric Fournet
Abstract. Polyphonic C ♯ is an extension of the C ♯ language with new asynchronous concurrency constructs, based on the join calculus. We describe the design and implementation of the language...
Modern Concurrency Abstractions for C (2002)
Nick Benton, Luca Cardelli, Cédric Fournet
Polyphonic C ♯ is an extension of the C ♯ language with new asynchronous concurrency constructs, based on the join calculus. We describe the design and implementation of the language and give...
A Spatial Logic for Concurrency (Part II) (2002)
Lus Caires And, Lus Caires, Luca Cardelli
this paper [2, 4] we study this intended model, which is used here to establish the soundness of the logical rules. The central focus of this Part II, however, is proof theory. We regularize and...
Modern Concurrency Abstractions for C (2002)
Nick Benton, Luca Cardelli, Abstract Polyphonic C
is an extension of the C language with new asynchronous concurrency constructs, based on the Join Calculus. We describe the design and implementation of the language and give examples of its use in...
A spatial logic for concurrency (part I (2001)
Abstract. We present a logic that can express properties of freshness, secrecy, structure, and behavior of concurrent systems. In addition to standard logical and temporal operators, our logic...
A Spatial Logic for Concurrency (Part I) (2001)
We present a logic that can express properties of freshness, secrecy, structure, and behavior of concurrent systems. In addition to standard logical and temporal operators, our logic includes spatial...
A query language based on the ambient logic (2001)
Abstract. The ambient logic is a modal logic proposed to describe the structural and computational properties of distributed and mobile computation. The structural part of the ambient logic is,...
A spatial logic for concurrency (part I (2001)
We present a logic that can express properties of freshness, secrecy, structure, and behavior of concurrent systems. In addition to standard logical and temporal operators, our logic includes spatial...
Secrecy and group creation (2000)
Luca Cardelli, Giorgio Ghelli, Andrew D. Gordon
Abstract. We add an operation of group creation to the typed-calculus, where a group is a type for channels. Creation of fresh groups has the e ect of statically preventing certain communications,...
Ambient Groups and Mobility Types (2000)
Luca Cardelli, Giorgio Ghelli, Andew D. Gordon, Andrew D. Gordon
. We add name groups and group creation to the typed ambient calculus. Group creation is surprisingly interesting: it has the effect of statically preventing certain communications, and can thus...
A Query Language for Semistructured Data Based on the Ambient Logic (2000)
The ambient logic is a modal logic proposed to describe the structural and computational properties of distributed and mobile computation. The structural part of the ambient logic is, essentially, a...
World Wide Web Conference. (2000)
Martin Abadi, Luca Cardelli, A Theory, Primitive Objects Untyped, David Atkins, Thomas Ball, ...
domain-specific language for form-based services. In: IEEE Transactions
Secrecy and group creation (2000)
Luca Cardelli, Giorgio Ghelli, Andrew D. Gordon
Abstract. We add an operation of group creation to the typed πcalculus, where a group is a type for channels. Creation of fresh groups has the effect of statically preventing certain communications,...
Abstract. The last decades have seen the emergence of the sea of objects paradigm for structuring complex distributed systems on workstations and local area networks. In this approach, applications...
Abstractions for mobile computation (1999)
Abstract. We discuss the difficulties caused by mobile computing and mobile computation over wide area networks. We propose a unified framework for overcoming such difficulties. 1
Abstractions for mobile computation (1999)
Abstract. We discuss the difficulties caused by mobile computing and mobile computation over wide area networks. We propose a unified framework for overcoming such difficulties. 1
Luca Cardelli, Andrew D. Gordon
Abstract. We discuss the computational aspects of wide area networks, and we describe various facets of a process calculus devised to embody mobility, security, and wide area network semantics. These...
We discuss the difficulties caused by mobile computing and mobile computation over wide-area networks. We propose a unified framework for overcoming such difficulties.
Mobility Types for Mobile Ambients (1999)
Luca Cardelli, Luca Cardelli, Giorgio Ghelli, Giorgio Ghelli, Andrew D. Gordon, Andrew D. Gordon
An ambient is a named cluster of processes and subambients, which moves as a group. The untyped ambient calculus is a process calculus in which ambients model a variety of concepts such as network...
Ambient Groups and Mobility Types (1999)
Luca Cardelli, Giorgio Ghelli, Andrew D. Gordon
We add name groups and group creation to the typed ambient calculus. Group creation is surprisingly interesting: it has the effect of statically preventing certain communications, and can thus block...
Mobility Types for Mobile Ambients (1999)
Luca Cardelli, Giorgio Ghelli, Andrew D. Gordon
. An ambient is a named cluster of processes and subambients, which moves as a group. We describe type systems able to guarantee that certain ambients will remain immobile, and that certain ambients...
Mobility Types for Mobile Ambients (1999)
Luca Cardelli, Giorgio Ghelli, Andrew D. Gordon
. An ambient is a named cluster of processes and subambients, which moves as a group. The untyped ambient calculus is a process calculus in which ambients model a variety of concepts such as network...
Equational Properties of Mobile Ambients (1999)
Andrew D. Gordon, Luca Cardelli
. The ambient calculus is a process calculus for describing mobile computation. We develop a theory of Morris-style contextual equivalence for proving properties of mobile ambients. We prove a...
Equational Properties of Mobile Ambients (1999)
Andrew D. Gordon, Luca Cardelli
The ambient calculus is a process calculus for describing mobile computation. We develop a theory of Morris-style contextual equivalence for proving properties of mobile ambients. We prove a context...
Types for mobile ambients (1999)
Luca Cardelli, Andrew D. Gordon
Java has demonstrated the utility of type systems for mobile code, and in particular their use and implications for security. Security properties rest on the fact that a well-typed Java program (or...
Comparing Object Encodings (1998)
Kim B. Bruce, Luca Cardelli, Benjamin C. Pierce
Recent years have seen the development of several foundational models for statically typed object-oriented programming. But despite their intuitive similarity, differences in the technical machinery...
Luca Cardelli Digital, Mobile Ambients, Luca Cardelli, Andrew D. Gordon
We introduce a calculus describing the movement of processes and devices, including movement through administrative domains. 1 Introduction There are two distinct areas of work in mobility: mobile...
Mobile Ambients, Luca Cardelli, Andrew D. Gordon
We introduce a calculus describing the movement of processes and devices, including movement through administrative domains. 1 Introduction There are two distinct areas of work in mobility: mobile...
Abstractions for Mobile Computation (1998)
ions for Mobile Computation Luca Cardelli August 1, 1998 Technical Report MSR-TR-98-34 Microsoft Research Microsoft Corporation One Microsoft Way Redmond, WA 1 Abstract. We discuss the difficulties...
Luca Cardelli, Andrew D. Gordon
We introduce a calculus describing the movement of processes and devices, including movement through administrative domains. Keywords: Agents, process calculi, mobility, wide-area computation. 1...
Types for Mobile Ambients (1998)
Luca Cardelli, Andrew D. Gordon
Java has demonstrated the utility of type systems for mobile code, and in particular their use and implications for security. Security properties rest on the fact that a well-typed Java program (or...
Comparing Object Encodings (1998)
Kim B. Bruce, Luca Cardelli, Benjamin C. Pierce
Recent years have seen the development of several foundational models for statically typed object-oriented programming. But despite their intuitive similarity, differences in the technical machinery...
Luca Cardelli, Andrew D. Gordon
We introduce a calculus describing the movement of processes and devices, including movement through administrative domains. 1
Abstractions for Mobile Computation (1998)
Abstract. We discuss the difficulties caused by mobile computing and mobile computation over wide area networks. We propose a unified framework for overcoming such difficulties. 1
Luca Cardelli, Andrew D. Gordon
Laboratory We introduce a calculus describing the movement of processes and devices, including movement through administrative domains.
Program fragments, linking, and modularization (1997)
work may not be copied or reproduced in whole or in part for any commercial purpose.
Program Fragments, Linking, and Modularization (1997)
Module mechanisms have received considerable theoretical attention, but the associated concepts of separate compilation and linking have not been emphasized. Anomalous module systems have emerged in...
Program Fragments, Linking, and Modularization (1997)
Luca Cardelli February, Luca Cardelli, Luca Cardelli
Module mechanisms have received considerable theoretical attention, but the associated concepts of separate compilation and linking have not been emphasized. Anomalous module systems have emerged in...
Mobile Ambient, Luca Cardelli, Luca Cardelli
Introduction This note describes a non-distributed implementation of the basic operations of the ambient calculus [1]. The implementation uses standard shared-memory concurrent programming technology...
Comparing Object Encodings (1997)
Kim Bruce Luca, Kim B. Bruce, Luca Cardelli, Benjamin C. Pierce
. Recent years have seen the development of several foundational models for statically typed object-oriented programming. But despite their intuitive similarity, differences in the technical...
type: A data type whose nature is kept hidden, in such a way that only a predetermined collection of operations can operate on it. Contravariant: A type that varies in the inverse direction from one...
Computation over planet-wide structures is hindered by administrative, architectural, and physical constraints. These problems are surmountable, but must be addressed by developing new models of...
Service Combinators for Web Computing (1997)
The World-Wide Web is rich in content and services, but access to these resources must be obtained mostly through manual browsers. We would like to be able to write programs that reproduce human...
Mobile Ambients -Annex- (1997)
Luca Cardelli, Andrew D. Gordon
We develop some theory of the ambient calculus, based on a labeled transition system, strong bisimilarity and contextual equivalence. The goal of this Annex to the main paper is to recast notions of...
Comparing Object Encodings (1997)
Kim Bruce, Luca Cardelli, Benjamin C. Pierce
Recent years have seen the development of several foundational models for statically typed object-oriented programming. But despite their intuitive similarity, differences in the technical machinery...
Mobile Ambient Synchronization (1997)
Introduction This note describes a non-distributed implementation of the basic operations of the ambient calculus [1]. The implementation uses standard shared-memory concurrent programming technology...
Mobile Ambient, Luca Cardelli, Luca Cardelli
Introduction This note describes a non-distributed implementation of the basic operations of the ambient calculus [1]. The implementation uses standard shared-memory concurrent programming technology...
Service Combinators for Web Computing (1997)
. The World-Wide Web is rich in content and services, but access to these resources must be obtained mostly through manual browsers. We would like to be able to write programs that reproduce human...
Luca Cardelli, Rowan Davies, Luca Cardelli, Rowan Davies
work may not be copied or reproduced in whole or in part for any commercial purpose.
Program fragments, linking, and modularization (1997)
work may not be copied or reproduced in whole or in part for any commercial purpose.
Notes on Nominal Calculi for Security and Mobility (1997)
Andrew D. Gordon, Luca Cardelli, Giorgio Ghelli
Abstract. There is great interest in applying nominal calculi—computational formalisms that include dynamic name generation—to the problems of programming, specifying, and verifying secure and...
Luca Cardelli, Rowan Davies, Luca Cardelli, Rowan Davies
work may not be copied or reproduced in whole or in part for any commercial purpose.
for procedural languages. ~ Object calculi for object-oriented languages.
The Hopkins Objects Group (1996)
Kim Bruce, Luca Cardelli, Gary T. Leavens, Benjamin Pierce
Giving types to binary methods causes significant problems for object-oriented language designers and programmers. This paper offers a comprehensive description of the problems arising from typing...
An Imperative Object Calculus (1996)
. We develop an imperative calculus of objects. Its main type constructor is the one for object types, which incorporate variance annotations and Self types. A subtyping relation between object types...
On Subtyping and Matching (1996)
. A relation between recursive object types, called matching, has been proposed as a generalization of subtyping. Unlike subtyping, matching does not support subsumption, but it does support...
Computation over planet-wide structures is hindered by administrative, architectural, and physical constraints. These problems are surmountable, but must be addressed by developing new models of...
s to recompile source code. Techniques have emerged to get some of the advantages of both off-line and on-line portability, such as just-in-time compilation and run-time linking. But the emphasis is...
s to recompile source code. Techniques have emerged to get some of the advantages of both off-line and on-line portability, such as just-in-time compilation and run-time linking. But the emphasis is...
An Interpretation of Objects and Object Types (1996)
Martín Abadi, Luca Cardelli, Ramesh Viswanathan
We present an interpretation of typed object-oriented concepts in terms of well-understood, purely procedural concepts. More precisely, we give a compositional subtypepreserving translation of a...
Krishna A. Bharat, Krishna A. Bharat, Luca Cardelli, Luca Cardelli
and research purposes provided that all such whole or partial copies include the following: a notice that such copying is by permission of the Systems Research Center of Digital Equipment Corporation...
An imperative object calculus (1995)
Abstract. We develop an imperative calculus of objects. Its main type constructor is the one for object types, which incorporate variance annotations and Self types. A subtyping relation between...
On subtyping and matching (1995)
Abstract. A relation between recursive object types, called matching, has been proposed as a generalization of subtyping. Unlike subtyping, matching does not support subsumption, but it does support...
Distributed Applications in a Hypermedia Setting (1995)
This paper addresses the issues involved in embedding distributed applications in a hypermedia web. In particular, we describe how applications generated in the Visual Obliq programming environment...
Obliq: A Language with Distributed Scope (1995)
Obliq is a lexically-scoped untyped interpreted language that supports distributed object-oriented computation. An Obliq computation may involve multiple threads of control within an address space,...
An imperative object calculus: Basic typing and soundness (1995)
We develop an imperative calculus of objects that is both tiny and expressive. Our calculus provides a minimal setting in which to study the operational semantics and the typing rules of...
Distributed Applications in a Hypermedia Setting (1995)
This paper addresses the issues involved in embedding distributed applications in a hypermedia web. In particular, we describe how applications generated in the Visual Obliq programming environment...
Krishna A. Bharat, Luca Cardelli
We introduce a new genre of user interface applications that can migrate from one machine to another, taking their user interface and application contexts with them, and continue from where they left...
An Imperative Object Calculus - Basic Typing and Soundness (1995)
We develop an imperative calculus of objects that is both tiny and expressive. Our calculus provides a minimal setting in which to study the operational semantics and the typing rules of...
Distributed Applications in a Hypermedia Setting (1995)
Krishna Bharat Graphics, Krishna Bharat, Luca Cardelli
This paper addresses the issues involved in embedding distributed applications in a hypermedia web. In particular, we describe how applications generated in the Visual Obliq programming environment...
Systems Research Center, Luca Cardelli, Benjamin Pierce
There are situations in programmingwhere some dynamic typing is needed, even in the presence of advanced static type systems. We investigate the interplay of dynamic types with other advanced type...
Krishna Bharat, Krishna A. Bharat, Luca Cardelli, Luca Cardelli
We introduce a new genre of user interface applications that can migrate from one machine to another, taking their user interface and application contexts with them, and continue from where they left...
A Language with Distributed Scope (1995)
Luca Cardelli Digital, Luca Cardelli
Obliq is a lexically-scoped, untyped, interpreted language that supports distributed object-oriented computation. Obliq objects have state and are local to a site. Obliq computations can roam over...
An Imperative Object Calculus - Basic Typing and Soundness (1995)
We develop an imperative calculus of objects that is both tiny and expressive. Our calculus provides a minimal setting in which to study the operational semantics and the typing rules of...
Kim B. Bruce, Luca Cardelli, Giuseppe Castagna, Jonathan Eifrig, Scott F. Smith, Valery Trifonov, ...
Giving types to binary methods causes significant problems for object-oriented language designers and programmers. This paper offers a comprehensive description of the problems arising from typing...
Kim Bruce, Luca Cardelli, Gary T. Leavens, Benjamin Pierce
This paper offers a comprehensive description of the problems arising from typing binary methods, and collects and contrasts diverse views and solutions. It summarizes the current debate on the...
Systems Research Center, Luca Cardelli, Benjamin Pierce
There are situations in programmingwhere some dynamic typing is needed, even in the presence of advanced static type systems. We investigate the interplay of dynamic types with other advanced type...
A Language with Distributed Scope (1995)
Obliq is a lexically-scoped, untyped, interpreted language that supports distributed object-oriented computation. Obliq objects have state and are local to a site. Obliq computations can roam over...
Gary T. Leavens, Benjamin Pierce, Giuseppe Castagna, Kim Bruce, Kim Bruce, ...
data types, modules, packages; F.3.1 [Logics and Meanings of Programs ] Specifying and Verifying and Reasoning about Programs --- logics of programs; F.3.2 [Logics and Meanings of Programs ] Studies...
Krishna A. Bharat, Luca Cardelli
We introduce a new genre of user interface applications that can migrate from one machine to another, taking their user interface and application contexts with them, and continue from where they left...
Kim Bruce, Kim Bruce, Luca Cardelli, Luca Cardelli, Gary T. Leavens, Gary T. Leavens, ...
data types, modules, packages; F.3.2 [Logics and Meanings of Programs] Studies of Program Constructs --- type structure. To appear in Theory and Practice of Object Systems. Copyright c fl assigned to...
We introduce a new genre of user interface applications that can migrate from one machine to another, taking their user interface and application contexts with them, and continue from where they left...
Distributed Applications in a Hypermedia Setting (1995)
This paper addresses the issues involved in embedding distributed applications in a hypermedia web. In particular, we describe how applications generated in the Visual Obliq programming environment...
Dynamic typing in polymorphic languages (1995)
Luca Cardelli, Benjamin Pierce, Robert W. Taylor
The charter of SRCistoadvance both the state of knowledge and the state of the art in computer systems. From our establishment in 1984, we have performed basic and applied research to support...
Krishna A. Bharat, Krishna A. Bharat, Luca Cardelli, Luca Cardelli
and research purposes provided that all such whole or partial copies include the following: a notice that such copying is by permission of the Systems Research Center of Digital Equipment Corporation...
Dynamic typing in polymorphic languages (1995)
Luca Cardelli, Benjamin Pierce, Robert W. Taylor
The charter of SRCistoadvance both the state of knowledge and the state of the art in computer systems. From our establishment in 1984, we have performed basic and applied research to support...
The Quest Language and System (1994)
2. System tutorial 3. The big picture 3.1. Kinds, types, and values 3.2. Signatures and bindings
A theory of primitive objects: Untyped and first-order systems (1994)
We introduce simple object calculi that support method override and object subsumption. We give an untyped calculus, typing rules, and equational rules. We illustrate the expressiveness of our...
Extensible records in a pure calculus of subtyping (1994)
Extensible records were introduced by Mitchell Wand while studying type inference in a polymorphic l-calculus with record types. This paper describes a calculus with extensible records, F r, that can...
A Semantics of Object Types (1994)
: We give a semantics for a typed object calculus, an extension of System F with object subsumption and method override. We interpret the calculus in a per model, proving the soundness of both typing...
A Semantics of Object Types (1994)
Martn Abadi And, Martn Abadi, Luca Cardelli
: We give a semantics for a typed object calculus, an extension of System F with object subsumption and method override. We interpret the calculus in a per model, proving the soundness of both typing...
A Theory of Primitive Objects - Untyped and First-Order Systems (1994)
We introduce simple object calculi that support method override and object subsumption. We give an untyped calculus, typing rules, and equational rules. We illustrate the expressiveness of our...
A Theory of Primitive Objects (1994)
We describe a second-order calculus of objects. The calculus supports object subsumption, method override, and the type Self. It is constructed as an extension of System F with subtyping, recursion,...
A Theory of Primitive Objects (1994)
Martin Abadi, Martn Abadi, Luca Cardelli
We investigate calculi that support method override in presence of object subsumption. Subsumption is the ability to emulate an object by means of another object that has more refined methods....
Obliq: A language with distributed scope (1994)
Obliq is a lexically-scoped untyped interpreted language that supports distributed objectoriented computation. An Obliq computation may involve multiple threads of control within an address space,...
Extensible Syntax with Lexical Scoping (1994)
Luca Cardelli, Florian Matthes, Martin Abadi, Robert W. Taylor
A frequent dilemma in programming language design is the choice between a language with a rich set of notations and a small, simple core language. We address this dilemma by proposing extensible...
Dynamic Typing in Polymorphic Languages (1994)
Martín Abadi, Luca Cardelli, Benjamin Pierce, Didier Rémy, Robert W. Taylor
There are situations in programmingwhere some dynamic typing is needed, even in the presence of advanced static type systems. We investigate the interplay of dynamic types with other advanced type...
Extensible records in a pure calculus of subtyping (1994)
Extensible records were introduced by Mitchell Wand while studying type inference in a polymorphic λ-calculus with record types. This paper describes a calculus with extensible records, F <:ρ,...
An extension of system F with subtyping (1994)
Luca Cardelli, Simone Martini, John C. Mitchell, Andre Scedrov
System F is a well-known typed λ-calculus with polymorphic types, which provides a basis for polymorphic programming languages. We study an extension of F, called F <: ּ(pronounced ּ ef-sub)...
An extension of system F with subtyping (1994)
Luca Cardelli, Simone Martini, John C. Mitchell, Andre Scedrov
System F is a well-known typed λ-calculus with polymorphic types, which provides a basis for polymorphic programming languages. We study an extension of F, called F <: (pronounced ef-sub) that...
This work may not be copied or reproduced in whole or in part for any commercial purpose. Permission to copy in whole or in part without payment of fee is granted for nonprofit educational and...
An extension of system F with subtyping (1994)
Luca Cardelli, Simone Martini, John C. Mitchell, Andre Scedrov
System F is a well-known typed λ-calculus with polymorphic types, which provides a basis for polymorphic programming languages. We study an extension of F, called F <: (pronounced ef-sub) that...
This work may not be copied or reproduced in whole or in part for any commercial purpose. Permission to copy in whole or in part without payment of fee is granted for nonprofit educational and...
Extensible syntax with lexical scoping (1994)
Luca Cardelli, Florian Matthes
The charter of SRCistoadvance both the state of knowledge and the state of the art in computer systems. From our establishment in 1984, we have performed basic and applied research to support...
Extensible grammars for language specialization (1993)
Luca Cardelli, Florian Ma, Tthes Martin Abadi
A frequent dilemma in the design of a database programming language is the choice between a language with a rich set of tailored notations for schema definitions, query expressions, etc., and a...
A logic for parametric polymorphism (1993)
Martín Abadi, Luca Cardelli, Pierre-louis Curien
A polymorphic function is parametric if its behavior does not depend on the type at which it is instantiated. Starting with Reynolds's work, the study of parametricity is typically semantic. In...
A logic for parametric polymorphism (1993)
Martín Abadi, Luca Cardelli, Pierre-louis Curien
A polymorphic function is parametric if its behavior does not depend on the type at which it is instantiated. Starting with Reynolds's work, the study of parametricity is typically semantic. In...
F-calculus with subtyping. This paper describes an implementation of F used. Using this implementation, one can test F tions. To facilitate the writing of complex F tension mechanism. New syntax can...
A logic for parametric polymorphism (1993)
Martín Abadi, Luca Cardelli, Pierre-louis Curien
A polymorphic function is parametric if its behavior does not depend on the type at which it is instantiated. Starting with Reynolds's work, the study of parametricity is typically semantic. In...
Subtyping recursive types (1993)
Roberto M. Amadio, Luca Cardelli
We investigate the interactions of subtyping and recursive types, in a simply typed l-calculus. The two fundamental questions here are whether two (recursive) types are in the subtype relation, and...
Subtyping Recursive Types (1993)
We investigate the interactions of subtyping and recursive types, in a simply typed l-calculus. The two fundamental questions here are whether two (recursive) types are in the subtype relation, and...
Formal Parametric Polymorphism (1993)
Martn Abadi Luca, Luca Cardelli, Pierre-louis Curien
A polymorphic function is parametric if its behavior does not depend on the type at which it is instantiated. Starting with Reynolds's work, the study of parametricity is typically semantic. In...
Formal Parametric Polymorphism (1993)
Mart Abadi, Luca Cardelli, Pierre-louis Curien
A polymorphic function is parametric if its behavior does not depend on the type at which it is instantiated. Starting with Reynolds's work, the study of parametricity is typically semantic. In...
Formal Parametric Polymorphism (1993)
Martin Abadi, Martn Abadi, Luca Cardelli, Pierre-Louis Curien
A polymorphic function is parametric if its behavior does not depend on the type at which it is instantiated. Starting with Reynolds's work, the study of parametricity is typically semantic. In...
Formal Parametric Polymorphism (1993)
Martin Abadi, Martn Abadi, Luca Cardelli, Pierre-Louis Curien
A polymorphic function is parametric if its behavior does not depend on the type at which it is instantiated. Starting with Reynolds's work, the study of parametricity is typically semantic. In...
There exists an identifiable programming style based on the widespread use of type information handled through mechanical typechecking techniques. This typeful programming style is in a sense...
Subtyping Recursive Types (1993)
Roberto Amadio Luca, Luca Cardelli
We investigate the interactions of subtyping and recursive types, in a simply typed l-calculus. The two fundamental questions here are whether two (recursive) types are in the subtype relation, and...
Luca Cardelli, John C. Mitchell
We define a simple collection of operations for creating and manipulating record structures, where records are intended as finite associations of values to labels. A second-order type system over...
Subtyping and Parametricity (1993)
In this paper we study the interaction of subtyping and parametricity. We describe a logic for a programming language with parametric polymorphism and subtyping. The logic supports the formal...
Subtyping and Parametricity (1993)
In this paper we study the interaction of subtyping and parametricity. We describe a logic for a programming language with parametric polymorphism and subtyping. The logic supports the formal...
Subtyping and Parametricity (1993)
Gordon Plotkin, Martín Abadi, Luca Cardelli
In this paper we study the interaction of subtyping and parametricity. We describe a logic for a programming language with parametric polymorphism and subtyping. The logic supports the formal...
Subtyping and Parametricity (1993)
Gordon Plotkin, Martin Abadi, Luca Cardelli
and parametricity. We describe a logic for a programming language with parametric polymorphism and subtyping. The logic supports the formal definition and use of relational parametricity. We give two...
Subtyping recursive types (1993)
Roberto M. Amadio, Luca Cardelli
We investigate the interactions of subtyping and recursive types, in a simply typed λ-calculus. The two fundamental questions here are whether two (recursive) types are in the subtype relation, and...
A logic for parametric polymorphism (1993)
Martín Abadi, Luca Cardelli, Pierre-louis Curien
A polymorphic function is parametric if its behavior does not depend on the type at which it is instantiated. Starting with Reynolds's work, the study of parametricity is typically semantic. In...
Subtyping recursive types (1993)
Roberto M. Amadio, Luca Cardelli
We investigate the interactions of subtyping and recursive types, in a simply typed λ-calculus. The two fundamental questions here are whether two (recursive) types are in the subtype relation, and...
F<: is a highly expressive typed λ-calculus with subtyping. This paper describes an implementation of F<: (extended with recursive types), and documents the algorithms used. Using this...
An implementation of F<: (1993)
F<: is a highly expressive typed l-calculus with subtyping. This paper describes an implementation of F<: (extended with recursive types), and documents the algorithms used. Using this...
Subtyping recursive types (1992)
Amadio, Roberto M., Cardelli, Luca
We investigate the interactions of subtyping and recursive types, in a simply typed lambda-calculus. The two fundamental questions here are whether two (recursive) types are in the subtype relation,...
Subtyping recursive types (1992)
Amadio, Roberto M., Cardelli, Luca
We investigate the interactions of subtyping and recursive types, in a simply typed lambda-calculus. The two fundamental questions here are whether two (recursive) types are in the subtype relation,...
Dynamic Typing in Polymorphic Languages (1992)
Martín Abadi, Luca Cardelli, Benjamin Pierce, Didier Rémy, Inria Rocquencourt
Types The interaction between the use of Dynamic and abstract data types gives rise to a puzzling design issue: should the type tag of a dynamically typed value containing an element of an abstract...
Luca Cardelli, John C. Mitchell
We define a simple collection of operations for creating and manipulating record structures, where records are intended as finite associations of values to labels. A second-order type system over...
Luca Cardelli, John C. Mitchell
We define a simple collection of operations for creating and manipulating record structures, where records are intended as finite associations of values to labels. A second-order type system over...
Luca Cardelli, John C. Mitchell
We define a simple collection of operations for creating and manipulating record structures, where records are intended as finite associations of values to labels. A second-order type system over...
We define a simple collection of operations for creating and manipulating record structures, where records are intended as finite associations of values to labels. A second-order type system over...
Extensible Records in a Pure Calculus of Subtyping (1991)
Extensible records were introduced by Mitchell Wand while studying type inference in a polymorphic l-calculus with record types. This paper describes a calculus with extensible records, F <: r,...
Systems Research Center (1991)
The Charter, Luca Cardelli, Florian Matthes, Robert W. Taylor
A frequent dilemma in programming language design is the choice between a language with a rich set of notations and a small, simple core language. We address this dilemma by proposing extensible...
An extension of system F with subtyping (1991)
Luca Cardelli, Simone Martini, John C. Mitchell, Andre Scedrov
System F is a well-known typed l-calculus with polymorphic types, which provides a basis for polymorphic programming languages. We study an extension of F, called F <: (pronounced ef-sub) that...
Extensible Records in a Pure Calculus of Subtyping (1991)
Extensible records were introduced by Mitchell Wand while studying type inference in a polymorphic l-calculus with record types. This paper describes a calculus with extensible records, F <: r,...
An extension of system F with subtyping (1991)
Luca Cardelli, Simone Martini, John C. Mitchell, Andre Scedrov
System F is a well-known typed l-calculus with polymorphic types, which provides a basis for polymorphic programming languages. We study an extension of F , called F <: (pronounced ef-sub) that...
A semantic basis for Quest (1991)
Quest is a programming language based on impredicative type quantifiers and subtyping within a three-level structure of kinds, types and type operators, and values. The semantics of Quest is rather...
A semantic basis for Quest (1991)
Quest is a programming language based on impredicative type quantifiers and subtyping within a three-level structure of kinds, types and type operators, and values. The semantics of Quest is rather...
Luca Cardelli, John C. Mitchell
We define a simple collection of operations for creating and manipulating record structures, where records are intended as finite associations of values to labels. A second-order type system over...
A semantic basis for Quest (1990)
Quest is a programming language based on impredicative type quantifiers and subtyping within a three-level structure of kinds, types and type operators, and values. The semantics of Quest is rather...
A semantic basis for Quest (1990)
Quest is a programming language based on impredicative type quantifiers and subtyping within a three-level structure of kinds, types and type operators, and values. The semantics of Quest is rather...
Abstract types and the dot notation (1990)
We investigate the use of the dot notation in the context of abstract types. The dot notation—that is, a.f referring to the operation f provided by the abstraction a—is used by programming...
There exists an identifiable programming style based on the widespread use of type information handled through mechanical typechecking techniques. This typeful programming style is in a sense...
There exists an identifiable programming style based on the widespread use of type information handled through mechanical typechecking techniques. This typeful programming style is in a sense...
There exists an identifiable programming style based on the widespread use of type information handled through mechanical typechecking techniques. This typeful programming style is in a sense...
There exists an identifiable programming style based on the widespread use of type information handled through mechanical typechecking techniques. This typeful programming style is in a sense...
Luca Cardelli Digital, Luca Cardelli
There exists an identifiable programming style based on the widespread use of type information handled through mechanical typechecking techniques. This typeful programming style is in a sense...
Dynamic Typing in a Statically Typed Language (1989)
Martín Abadi, Luca Cardelli, Benjamin Pierce, Gordon Plotkin
Statically typed programming languages allow earlier error checking, better enforcement of disciplined programming styles, and generation of more efficient object code than languages where all type...
Dynamic Typing in a Statically Typed Language (1989)
Mart'in Abadi Luca, Luca Cardelli, Benjamin Pierce, Gordon Plotkin
Statically typed programming languages allow earlier error checking, better enforcement of disciplined programming styles, and generation of more efficient object code than languages where all type...
The Modula-3 Type System (1989)
Luca Cardelli, Jim Donahue, Mick Jordan, Bill Kalsow, Greg Nelson
This paper presents an overview of the programming language Modula-3, and a more detailed description of its type system. 1 Introduction The design of the programming language Modula-3 was a joint...
Dynamic Typing in a Statically Typed Language (1989)
Mart'in Abadi Luca, Luca Cardelli, Benjamin Pierce, Gordon Plotkin
Statically typed programming languages allow earlier error checking, better enforcement of disciplined programming styles, and generation of more efficient object code than languages where all type...
Dynamic Typing in a Statically Typed Language (1989)
Mart'in Abadi, Luca Cardelli, Benjamin Pierce, Gordon Plotkin
Statically typed programming languages allow earlier error checking, better enforcement of disciplined programming styles, and generation of more efficient object code than languages where all type...
There exists an identifiable programming style based on the widespread use of type information handled through mechanical typechecking techniques. This typeful programming style is in a sense...
A semantics of multiple inheritance (1988)
There are two major ways of structuring data in programming languages. The first and common one, used for example in Pascal, can be said to derive from standard branches of mathematics. Data is...
Building User Interfaces by Direct Manipulation (1988)
without payment of fee is granted for nonprofit educational and research purposes provided that all such whole or partial copies
Building User Interfaces by Direct Manipulation (1988)
acknowledgment of the authors and individuals contributors to the work; and all applicable portions of the copyright notice. Copying, reproducing, or republishing for any other purpose shall require...
Phase distinctions in type theory (1988)
Type systems were originally introduced in programming languages to provide a degree of static checking, achieved through typechecking. As type systems become more complex and typechecking more...
Structural Subtyping and the Notion of Power Type (1988)
Many statically and dynamically typed languages attempt to achieve flexibility in their type discipline by some notion of
Phase Distinctions in Type Theory (1988)
this paper we present a phase-free system based on dependent types, and then we modify it to obtain a phased system, which can be used as the basis of a compilable programming language.
Types for Data-Oriented Languages (1988)
Overview Luca Cardelli, Luca Cardelli
this paper is that kind structures should be of benefit in understanding and developing data-oriented languages.
A Semantics of Multiple Inheritance (1988)
this paper is to present a clean semantics of multiple inheritance and to show that, in the context of strongly-typed, statically-scoped languages, a sound typechecking algorithm exists. Multiple...
Structural Subtyping and the Notion of Power Type (1988)
Luca Cardelli Digital, Luca Cardelli
types We have used the term abstract type for types of the form P = Some(A:Type) B, because this models the concept of having an unknown type A which supports a set of operations of signature B. It...
A Semantics of Multiple Inheritance (1988)
Luca Cardelli Att, Luca Cardelli
this paper is to present a clean semantics of multiple inheritance and to show that, in the context of strongly-typed, statically-scoped languages, a sound typechecking algorithm exists. Multiple...
Phase Distinctions in Type Theory (1988)
this paper we present a phase-free system based on dependent types, and then we modify it to obtain a phased system, which can be used as the basis of a compilable programming language.
Building User Interfaces by (1988)
Direct Manipulation Luca, Luca Cardelli
this paper achieves this goal by separating the user interface from the application program, as is done in many user interface management systems [Pfaff 83], and by using a user interface editor to...
Basic Polymorphic Typechecking (1988)
This paper is largely concerned with implicit polymorphism; it is nonetheless important to dedicate the rest of this section to the relationships between the two kinds of parametric polymorphism.
Structural Subtyping and the Notion of Power Type (1988)
types We have used the term abstract type for types of the form P = Some(A:Type) B, because this models the concept of having an unknown type A which supports a set of operations of signature B. It...
Types for Data-Oriented Languages (1988)
this paper is that kind structures should be of benefit in understanding and developing data-oriented languages.
Basic Polymorphic Typechecking (1987)
Luca Cardelli Att, Luca Cardelli
This paper is largely concerned with implicit polymorphism; it is nonetheless important to dedicate the rest of this section to the relationships between the two kinds of parametric polymorphism.
A polymorphic l-calculus with Type:Type (1986)
payment of fee is granted for nonprofit educational and research purposes provided that all such whole or partial copies include the
Calculus With Type, Luca Cardelli
This paper describes a type-theoretical and denotational semantics foundation for Pebble-like languages.
A Polymorphic lambda-calculus with Type:Type (1986)
This paper describes a type-theoretical and denotational semantics foundation for Pebble-like languages.
A Polymorphic lambda-calculus with Type:Type (1986)
Introduction Ever since the notion of type was introduced in computer science, there have been people claiming that Type (the collection of all types) should be a type, and hence be a member of...
Introduction The Amber language embeds many recent ideas in programming language design, and tries to introduce all the features in their minimal, essential, form. One of its main goals is to safely...
A polymorphic l-calculus with Type:Type (1986)
acknowledgment of the authors and individuals contributors to the work; and all applicable portions of the copyright notice. Copying, reproducing, or republishing for any other purpose shall require...
A polymorphic l-calculus with Type:Type (1986)
acknowledgment of the authors and individuals contributors to the work; and all applicable portions of the copyright notice. Copying, reproducing, or republishing for any other purpose shall require...
On understanding types, data abstraction, and polymorphism (1985)
Our objective is to understand the notion of type in programming languages, present a model of typed, polymorphic programming languages that reflects recent research in type theory, and examine the...
On understanding types, data abstraction, and polymorphism (1985)
Our objective is to understand the notion of type in programming languages, present a model of typed, polymorphic programming languages that reflects recent research in type theory, and examine the...
On understanding types, data abstraction, and polymorphism (1985)
Our objective is to understand the notion of type in programming languages, present a model of typed, polymorphic programming languages that reflects recent research in type theory, and examine the...
Squeak: A Language for Communicating with Mice (1985)
Graphical user interfaces are difficult to implement because of the essential concurrency among multiple interaction devices, such as mice, buttons, and keyboards. Squeak is a user interface...
Galileo: A Strongly Typed, Interactive Conceptual Language (1985)
Antonio Albano, Luca Cardelli, Renzo Orsini
Galileo, a programming language for database applications, is presented. Galileo is a strongly typed, interactive programming language designed specifically to support Semantic Data Model features...
On Understanding Types, Data Abstraction, and Polymorphism (1985)
Luca Cardelli Att, Luca Cardelli, Peter Wegner
ion, and Polymorphism Luca Cardelli AT&T Bell Laboratories, Murray Hill, NJ 07974 (current address: DEC SRC, 130 Lytton Ave, Palo Alto CA 94301) Peter Wegner Dept. of Computer Science, Brown...
On Understanding Types, Data Abstraction, and Polymorphism (1985)
Our objective is to understand the notion of type in programming languages, present a model of typed, polymorphic programming languages that reflects recent research in type theory, and examine the...
On Understanding Types, Data Abstraction, and Polymorphism (1985)
ion, and Polymorphism Luca Cardelli AT&T Bell Laboratories, Murray Hill, NJ 07974 (current address: DEC SRC, 130 Lytton Ave, Palo Alto CA 94301) Peter Wegner Dept. of Computer Science, Brown...
On understanding types, data abstraction, and polymorphism (1985)
Our objective is to understand the notion of type in programming languages, present a model of typed, polymorphic programming languages that reflects recent research in type theory, and examine the...
On understanding types, data abstraction, and polymorphism (1985)
Our objective is to understand the notion of type in programming languages, present a model of typed, polymorphic programming languages that reflects recent research in type theory, and examine the...
On understanding types, data abstraction, and polymorphism (1985)
Our objective is to understand the notion of type in programming languages, present a model of typed, polymorphic programming languages that reflects recent research in type theory, and examine the...
Compiling a Functional Language (1984)
Luca Cardelli Att, Luca Cardelli
Machine The Functional Abstract Machine (Fam) is a stack machine designed to support functional languages on large address space computers. It can be considered an SECD machine [Landin 64] which has...
Compiling a Functional Language (1984)
Luca Cardelli Att, Luca Cardelli
Machine The Functional Abstract Machine (Fam) is a stack machine designed to support functional languages on large address space computers. It can be considered an SECD machine [Landin 64] which has...
An Implementation Model of Rendezvous Communication (1984)
Luca Cardelli Att, Luca Cardelli
This paper describes the low-level primitives necessary to implement a particular flavor or inter-process communication. It is motivated by the design of a communication subsystem for a higher-order...
Compiling a Functional Language (1984)
Machine The Functional Abstract Machine (Fam) is a stack machine designed to support functional languages on large address space computers. It can be considered an SECD machine [Landin 64] which has...
The Functional Abstract (1983)
Luca Cardelli, Andrew D. Gordon
We present a commitment relation, a kind of labeled transition system, for the ambient calculus. This note is an extract from an unpublished annex to our original article [2] on the ambient calculus....
An algebraic approach to hardware description and verification / (1982)
Thesis (Ph. D.)--University of Edinburgh, 1982.
From Processes to ODEs by Chemistry (1970)
We investigate the collective behavior of processes in terms of differential equations, using chemistry as a stepping stone. Chemical reactions can be converted to ordinary differential equations,...
A Theory of Primitive Objects - Second-Order Systems
We describe a second-order calculus of objects. The calculus supports object subsumption, method override, and the type Self. It is constructed as an extension of System F with subtyping, recursion,...
Luca Cardelli Att, Luca Cardelli
The Amber machine is a stack machine designed as an intermediate language for compiling higher-order languages. The current version is specialized for the Amber language. The machine supports a set...
The Amber machine is a stack machine designed as an intermediate language for compiling higher-order languages. The current version is specialized for the Amber language. The machine supports a set...
Compositionality, stochasticity, and cooperativity in dynamic models of gene regulation
Blossey, Ralf, Cardelli, Luca, Phillips, Andrew
We present an approach for constructing dynamic models for the simulation of gene regulatory networks from simple computational elements. Each element is called a “gene gate” and defines an...