The Design of Distributed Programming Languages (2008)
Peter Sewell, John Billings, Steve Bishop, Matthew Fairbairn, Pierre Habouzit, Michael Hicks, ...
High-level programming languages For non-distributed, non-concurrent programming, they’re pretty good. We have ML (SML/OCaml), Haskell, Java, C#, with: • type safety • rich concrete types –...
Author’s Guide to the ACM SIGPLAN Class (sigplanconf.cls) Association for Computing Machinery (2008)
Class Paul, C. Anagnostopoulos, Windfall Software, Guide Paul, C. Anagnostopoulos, ...
The programs and applications presented in this book have been included for their instructional value. They have been tested with care, but are not guaranteed for any particular purpose. The...
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
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...
Martin Hofmann, Benjamin Pierce
We give a direct type-theoretic characterization of the basic mechanisms of object-oriented programming, including objects, methods, message passing, and subtyping, by introducing an explicit...
Author’s Guide to the ACM SIGPLAN Class (sigplanconf.cls) Association for Computing Machinery (2007)
Class Paul, C. Anagnostopoulos, Windfall Software, Guide Paul, C. Anagnostopoulos, ...
The programs and applications presented in this book have been included for their instructional value. They have been tested with care, but are not guaranteed for any particular purpose. The...
• Type Checking For Functional XML Programming (2006)
Mukund Raghavachari, Copyright C, Mukund Raghavachari, John Evdemon, Vladimir Gapeyev, François Garillot, ...
Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy. See back inner page for a list of recent BRICS...
Regular expression types for XML (2005)
Hosoya, Haruo, Vouillon, Jérôme, Pierce, Benjamin
We propose regular expression types as a foundation for statically typed XML processing languages. Regular expression types, like most schema languages for XML, introduce regular expression notations...
Chorus & Maestro: Distributed Synchronization (2005)
Matthew Jones, Jacob Wiseman, Faculty Advisors Fern, O Pereira, Benjamin Pierce
Carmem Satie Hara, Susan Davidson, Wenfei Fan, Benjamin Pierce
To my parents. ii To Wagner and Pedro. iii
Algorithms for Distributed and Mobile Sensing (2004)
Ibrahim Volkan Isler, Benjamin Pierce, Kostas Daniilidis, Kostas Daniilidis, ...
ALGORITHMS FOR DISTRIBUTED AND MOBILE SENSING Ibrahim Volkan Is . ler Kostas Daniilidis and Sampath Kannan Sensing remote, complex and large environments is an important task that arises in diverse...
FAITHFUL IDEAL MODELS FOR RECURSIVE POLYMORPHIC TYPES (2003)
Abadi, Martin, Pierce, Benjamin, Plotkin, Gordon
We explore ideal models for a programming language with recursive polymorphic types, variants of the model studied by MacQueen, Plotkin, and Sethi. The use of suitable ideals yields a close fit...
FAITHFUL IDEAL MODELS FOR RECURSIVE POLYMORPHIC TYPES (2003)
Abadi, Martin, Pierce, Benjamin, Plotkin, Gordon
We explore ideal models for a programming language with recursive polymorphic types, variants of the model studied by MacQueen, Plotkin, and Sethi. The use of suitable ideals yields a close fit...
Dimitris Metaxas, Benjamin Pierce, Siome Goldenstein, Siome Goldenstein
In memory of my grandmother, Nehama Klein. iii Acknowledgments It is challenging to list in one single place all the people who directly or indirectly helped me throughout my years at Penn. I may be...
Siome Goldenstein, Dimitris Metaxas, Benjamin Pierce, Siome Goldenstein
In memory of my grandmother, Nehama Klein. iii Acknowledgments It is challenging to list in one single place all the people who directly or indirectly helped me throughout my years at Penn. I may be...
Regular expression pattern matching for XML (2001)
We propose regular expression pattern matching as a core feature for programming languages for manipulating XML (and similar tree-structured data formats). We extend conventional pattern-matching...
Regular expression pattern matching for XML (2001)
We propose regular expression pattern matching as a core feature for programming languages for manipulating XML (and similar tree-structured data formats). We extend conventional pattern-matching...
Tree Automata and Pattern Matching (2000)
Tree automata have been used both in program analyses for functional languages and in type systems for tree-like data such as SGML and XML. They also form a natural basis for rich forms of pattern...
Relating Cryptography and Polymorphism (2000)
Cryptography is information hiding. Polymorphism is also information hiding. So is cryptography polymorphic? Is polymorphism cryptographic? To investigate these questions, we dene the cryptographic...
XDuce: A Typed XML Processing Language (Preliminary Report) (2000)
Haruo Hosoya And, Haruo Hosoya, Benjamin Pierce
this paper, we present a preliminary design for a statically typed programming language, XDuce (pronounced "transduce"). XDuce is a tree transformation language, similar in spirit to...
Relating Cryptography and Polymorphism (2000)
Cryptography is information hiding. Polymorphism is also information hiding. So is cryptography polymorphic? Is polymorphism cryptographic? To investigate these questions, we define the cryptographic...
Recursive Subtyping Revealed (2000)
Vladimir Gapeyev, Michael Levin, Benjamin Pierce
Algorithms for checking subtyping between recursive types lie at the core of many programming language implementations. But the fundamental theory of these algorithms and how they relate to simpler...
Relating Cryptography and Polymorphism (2000)
Benjamin Pierce Eijiro, Benjamin Pierce, Eijiro Sumii
Cryptography is information hiding. Polymorphism is also information hiding. So is cryptography polymorphic? Is polymorphism cryptographic? To investigate these questions, we define the cryptographic...
Relating cryptography and polymorphism (2000)
Cryptography is information hiding. Polymorphism is also information hiding. So is cryptography polymorphic? Is polymorphism cryptographic? To investigate these questions, we define the cryptographic...
Union Types for Semistructured Data (1999)
Peter Buneman, Benjamin Pierce
Semistructured databases are treated as dynamically typed: they come equipped with no independent schema or type system to constrain the data. Query languages that are designed for semistructured...
Featherweight Java - A Minimal Core Calculus for Java and GJ (1999)
Atsushi Igarashi, Benjamin Pierce, Philip Wadler
Several recent studies have introduced lightweight versions of Java: reduced languages in which complex features like threads and reflection are dropped to enable rigorous arguments about key...
Union Types for Semistructured Data (1999)
Peter Buneman, Benjamin Pierce
Semistructured databases are treated as dynamically typed: they come equipped with no independent schema or type system to constrain the data. Query languages that are designed for semistructured...
Featherweight Java - A Minimal Core Calculus for Java and GJ (1999)
Atsushi Igarashi, Benjamin Pierce, Philip Wadler
Several recent studies have introduced lightweight versions of Java: reduced languages in which complex features like threads and reflection are dropped to enable rigorous arguments about key...
Local Type Argument Synthesis with Bounded Quantification (1997)
Benjamin Pierce, David N. Turner, An Teallach Limited
In a companion paper [PT98], we introduced a local type inference method for inferring type arguments to polymorphic functions. We show here how our method can be extended to handle Cardelli and...
Pict: A Programming Language Based on the Pi-Calculus (1997)
Benjamin Pierce, David N. Turner
The ß-calculus offers an attractive basis for concurrent programming. It is small, elegant, and well studied, and supports (via simple encodings) a wide range of high-level constructs including data...
Typing and subtyping for mobile processes (1996)
Benjamin Pierce, Davide Sangiorgi
The-calculus is a process algebra that supports process mobility by focusing on the communication of channels. Milner's presentation of the-calculus includes a type system assigning arities to...
Typing and subtyping for mobile processes (1996)
Benjamin Pierce, Davide Sangiorgi
The-calculus is a process algebra that supports process mobility by focusing on the communication of channels. Milner's presentation of the-calculus includes a type system assigning arities to...
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...
Martin Hofmann, Benjamin Pierce
The statement S T in a-calculus with subtyping is traditionally interpreted as a semantic coercion function of type [[S]]![[T]] that extracts the "T part " of an element of S. If...
Bounded Existentials and Minimal Typing (1996)
Giorgio Ghelli, Benjamin Pierce
We study an extension of the second-order calculus of bounded quantification, System F , with bounded existential types. Surprisingly, the most natural formulation of this extension lacks the...
Typing and Subtyping for Mobile Processes (1996)
Benjamin Pierce, Davide Sangiorgi
The ß-calculus is a process algebra that supports process mobility by focusing on the communication of channels. Milner's presentation of the ß-calculus includes a type system assigning...
Typing and Subtyping for Mobile Processes (1996)
Benjamin Pierce, Davide Sangiorgi
The pi-calculus is a process algebra that supports process mobility by focusing on the communication of channels. Milner's presentation of the pi-calculus includes a type system assigning...
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...
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...
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...
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...
Concurrent Objects in a Process Calculus (1995)
Benjamin Pierce, David N. Turner
A programming style based on concurrent objects arises almost inevitably in languages where processes communicate by exchanging data on channels. Using the Pict language as an experimental testbed,...
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...
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...
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...
Martin Hofmann, Benjamin Pierce
this paper, we have assigned meaning to terms by giving a PER model providing both a simple operational semantics and justification of a set of equational rules. For larger calculi (including, for...
Higher-order Subtyping, Martin Steffen, Benjamin Pierce, Interner Bericht Immd
System F ! is an extension with subtyping of Girard's higher-order polymorphic -calculus. We develop the fundamental metatheory of this calculus: decidability of fi-conversion on well-kinded...
A Unifying Type-Theoretic Framework for Objects (1993)
Martin Hofmann, Benjamin Pierce
We give a direct type-theoretic characterization of the basic mechanisms of object-oriented programming, including objects, methods, message passing, and subtyping, by introducing an explicit...
Statically Typed Friendly Functions via Partially Abstract Types (1993)
A well-known shortcoming of the object model of Simula and Smalltalk is the inability to deal cleanly with methods that require access to the internal state of more than one object at a time. Recent...
Typing and Subtyping for Mobile Processes (Extended Abstract) (1992)
Benjamin Pierce, Davide Sangiorgi
The -calculus is a process algebra that supports process mobility by focusing on the communication of channels. Milner's presentation of the -calculus includes a type system assigning arities to...
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...
Faithful ideal models for recursive polymorphic types (1991)
Mart In Abadi, Benjamin Pierce, Gordon Plotkin
We explore ideal models for a programming language with recursive polymorphic types, variants of the model studied by MacQueen, Plotkin, and Sethi. The use of suitable ideals yields a close fit...
Faithful ideal models for recursive polymorphic types (1991)
Mart Abadi, Benjamin Pierce, Gordon Plotkin
We explore ideal models for a programming language with recursive polymorphic types, variants of the model studied by MacQueen, Plotkin, and Sethi. The use of suitable ideals yields a close t between...
Faithful Ideal Models for Recursive Polymorphic Types (1991)
Martín Abadi, Benjamin Pierce, Gordon Plotkin
We explore ideal models for a programming language with recursive polymorphic types, variants of the model studied by MacQueen, Plotkin, and Sethi. The use of suitable ideals yields a close fit...
Programming with Intersection Types and Bounded Polymorphism (1991)
Intersection types and bounded quantification are complementary mechanisms for extending the expressive power of statically typed programming languages. They begin with a common framework: a simple,...
A Record Calculus Based on Symmetric Concatenation (1991)
Robert Harper, Benjamin Pierce
Type systems for operations on extensible records form a foundation for statically typed languages addressing some aspects of object oriented programming and database applications. A number of...
Faithful ideal models for recursive polymorphic types (1991)
Martín Abadi, Benjamin Pierce, Gordon Plotkin
We explore ideal models for a programming language with recursive polymorphic types, variants of the model studied by MacQueen, Plotkin, and Sethi. The use of suitable ideals yields a close fit...
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...
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...
Faithful Ideal Models for Recursive Polymorphic Types (1989)
Martín Abadi, Benjamin Pierce, Gordon Plotkin
We explore ideal models for a programming language with recursive polymorphic types, variants of the model studied by MacQueen, Plotkin, and Sethi. The use of suitable ideals yields a close fit...
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...