Abstract Stability Issues in OSPF Routing (2008)
We study the stability of the OSPF protocol under steady state and perturbed conditions. We look at three indicators of stability, namely, (a) network convergence times, (b) routing load on...
The SLam calculus is a typed-calculus that maintains security information as well as type information. The type system propagates security information for each objectinfourforms: the object's...
Column Editor Jon, Jon G. Riecke, Peter W. O'hearn
Types Peter W. O'Hearn Department of Computer Science Queen Mary & Westfield College (ohearn@dcs.qmw.ac.uk) October 7, 1998 1 Introduction Abstraction is one of the pillars of computer...
A Relational Account of (2007)
Anders B. Sandholm, Jon G. Riecke, Jon G. Riecke
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 Report Series publications. Copies may be...
Data Integration in Vector (Vertically Partitioned) Databases Peter Buneman (2007)
Peter Buneman, Jon G. Riecke, Eric Sandler, Vladimir Seroff, Aleri Inc
Data integration requires not only the absorption of data, but the transformation of that data. For instance, manufacturing companies must combine customer order information for ordering supplies as...
A Calculus for Compiling and Linking Classes (2000)
Kathleen Fisher, John Reppy, Jon G. Riecke
. We describe ink& (pronounced "links"), a low-level calculus designed to serve as the basis for an intermediate representation in compilers for class-based object-oriented languages....
A Calculus for Compiling and Linking Classes (2000)
Kathleen Fisher, John Reppy, Jon G. Riecke
. We describe a low-level calculus, called ink& (pronounced "links"), designed to serve as an intermediate representation in compilers for class-based objectoriented languages. The...
A calculus for compiling and linking classes (2000)
Kathleen Fisher, Jon G. Riecke
Abstract. We describe ink&(pronounced “links”), a low-level calculus designed to serve as the basis for an intermediate representation in compilers for class-based object-oriented languages....
A calculus for compiling and linking classes (2000)
Kathleen Fisher, Jon G. Riecke
Abstract. We describe a low-level calculus, called λinkς (pronounced “links”), designed to serve as an intermediate representation in compilers for class-based objectoriented languages. The...
Region analysis and the polymorphic lambda calculus (1999)
Anindya Banerjee, Nevin Heintze, Jon G. Riecke
We show how to translate the region calculus of Tofte and Talpin, a typed lambda calculus that can statically delimit the lifetimes of objects, into an extension of the polymorphic lambda calculus...
Region analysis and the polymorphic lambda calculus (1999)
Anindya Banerjee, Nevin Heintze, Jon G. Riecke
We show how to translate the region calculus of Tofte and Talpin, a typed lambda calculus which can statically delimit the lifetimes of objects, into an extension of the polymorphic lambda calculus...
A Core Calculus of Dependency (1999)
Martn Abadi Systems, Martn Abadi, Anindya Banerjee, Nevin Heintze, Jon G. Riecke
Notions of program dependency arise in many settings: security, partial evaluation, program slicing, and call-tracking. We argue that there is a central notion of dependency common to these settings...
A Core Calculus of Dependency (1999)
Martín Abadi, Anindya Banerjee, Nevin Heintze, Jon G. Riecke
Notions of program dependency arise in many settings: security, partial evaluation, program slicing, and call-tracking. We argue that there is a central notion of dependency common to these settings...
Typed Exceptions and Continuations Cannot Macro-Express Each Other (1999)
Jon Riecke And, Jon G. Riecke, Hayo Thielecke
. The most powerful control constructs in modern programming languages are continuations and exceptions. Although they can be used interchangeably in some cases, they are fundamentally different...
A Core Calculus of Dependency (1999)
Martn Abadi Systems, Martn Abadi, Anindya Banerjee, Nevin Heintze, Jon G. Riecke
Notions of program dependency arise in many settings: security, partial evaluation, program slicing, and call-tracking. We argue that there is a central notion of dependency common to these settings...
A Calculus for Compiling and Linking Classes (1999)
Kathleen Fisher, John Reppy, Jon G. Riecke
In this paper we present ink& (pronounced "links"), a low-level calculus designed to serve as an intermediate representation in compilers for class-based object-oriented languages. The...
Typed Exceptions and Continuations Cannot Macro-Express Each Other (1999)
. The most powerful control constructs in modern programming languages are continuations and exceptions. Although they can be used interchangeably in some cases, they are fundamentally different...
Typed Exceptions and Continuations Cannot Macro-Express Each Other (1999)
Jon Riecke And, Jon G. Riecke, Hayo Thielecke
. The most powerful control constructs in modern programming languages are continuations and exceptions. Although they can be used interchangeably in some cases, they are fundamentally different...
Region Analysis and the Polymorphic Lambda Calculus (1999)
Anindya Banerjee, Nevin Heintze, Jon G. Riecke
We show how to translate the region calculus of Tofte and Talpin, a typed lambda calculus which can statically delimit the lifetimes of objects, into an extension of the polymorphic lambda calculus...
Continuations, Functions and Jumps (1999)
this article, therefore, is to help the reader uncompress the CPS transform by way of a rational reconstruction from jumps.
Should a Function Continue? (1998)
We show that two lambda-calculus terms can be observationally congruent (i.e., agree in all contexts) but their continuation-passing transforms may not be. We also show that two terms may be...
Return types for functional continuations (1998)
We study the typing of control operators in a language with an ML-style type system. We introduce a new set of control operators that subsume most control operators that have been proposed for...
Privacy via Subsumption (1998)
Jon G. Riecke, Christopher A. Stone
types can be used to hide the representations of objects from 12 THEORY AND PRACTICE OF OBJECT SYSTEMS---??? clients, even though the objects themselves have access to the internal representations....
The SLam Calculus: Programming with Secrecy and Integrity (1998)
The SLam calculus is a typed -calculus that maintains security information as well as type information. The type system propagates security information for each object in four forms: the...
Conditions for the Completeness of Functional and Algebraic Equational Reasoning (1998)
Jon G. Riecke, Ramesh Subrahmanyam
We consider the following question: in the simply-typed l-calculus with algebraic operations, is the set of equations valid in a particular model exactly those provable from (b), (h), and the set of...
Privacy via Subsumption (1998)
Jon G. Riecke, Christopher A. Stone
We describe an object calculus that allows both extension of objects and full width subtyping (hiding arbitrary components). In contrast to other proposals, the types of our calculus do not mention...
Return Types for Functional Continuations (1998)
Carl Gunter, Didier Rémy, Jon G. Riecke
We add functional continuations and prompts to a language with an ML-style type system. The operators extend and simplify the control operators in Standard ML of New Jersey (SML/NJ) and Scheme, and...
The SLam Calculus: Programming with Secrecy and Integrity (1998)
We describe the SLam calculus, a typed -calculus that maintains security information as well as type information. The type system propagates both secrecy and integrity, maintaining four distinct...
The SLam Calculus: Programming with Security and Integrity (1998)
We describe the SLam calculus, a typed -calculus that maintains security information as well as type information. The calculus maintains four different forms of security information: which agents...
Return Types for Functional Continuations (1998)
I completely changed the abstract to reflect the new structure and emphasis of the paper] We study the typing of control operators in a language with an ML-style type system. We introduce a new set...
A relational account of call-by-value sequentiality (1997)
Anders B. Sandholm, Jon G. Riecke, Jon G. Riecke, Anders Sandholm
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 Report Series publications. Copies may be...
The Analysis of Programming Structure (1997)
This paper has explored three examples of good semantical analyses of programming structures. The three examples share two characteristics: the semantic models are abstract enough to be applicable in...
Semantic Orthogonality of Type Disciplines (1997)
Jon G. Riecke, Ramesh Subrahmanyam
We consider a version of PCF, and prove, using both syntactic and semantic means, that the operational equivalences of the base language are preserved when the language is extended with sum and...
Conditions for the Completeness of Functional and Algebraic Equational Reasoning (1997)
Jon G. Riecke, Ramesh Subrahmanyam
We consider the following problem in proving equations in models of functional languages: given a call-by-name language based on the simplytyped -calculus with algebraic operations axiomatized by...
A Relational Account of Call-by-Value Sequentiality (1997)
Jon G. Riecke, Anders Sandholm
We construct a model for FPC, a purely functional, sequential, call-by-value language. The model is built from partial continuous functions, in the style of Plotkin, further constrained to be uniform...
A Relational Account of Call-by-Value Sequentiality (1997)
Jon G. Riecke, Anders Sandholm
We construct a model for FPC, a purely functional, sequential, call-by-value language. The model is built from partial continuous functions, in the style of Plotkin, further constrained to be uniform...
A relational account of call-by-value sequentiality (1997)
Anders B. Sandholm, Jon G. Riecke, Jon G. Riecke, Anders Sandholm
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...
A relational account of call-by-value sequentiality (1997)
Anders B. Sandholm, Copyright C, Anders B. S, Jon G. Riecke, Jon G. Riecke, Jon G. Riecke, ...
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...
Reference Counting as a Computational Interpretation of Linear Logic (1996)
Jawahar Chirimar, Carl A. Gunter, Jon G. Riecke
We develop formal methods for reasoning about memory usage at a level of abstraction suitable for establishing or refuting claims about the potential applications of linear logic for static analysis....
Classes in Object ML via Modules (1996)
This paper describes a simple means for encoding classes in Object ML (OML) [RR96] using the Standard ML (SML) module system [Mac86]. In previous work [RR96], we showed how to mimic class-based...
A generalization of exceptions and control in ML-like languages (1995)
We add functional continuations and prompts to a language with an ML-style type system. The operators significantly extend and simplify the control operators in SML/NJ, and can be themselves used to...
A Generalization of Exceptions and Control in ML-like Languages (1995)
Carl Gunter, Didier Rémy, Jon G. Riecke
We add functional continuations and prompts to a language with an ML-style type system. The operators significantly extend and simplify the control operators in SML/NJ, and can be themselves used to...
Isolating Side Effects in Sequential Languages (1995)
Jon G. Riecke, Ramesh Viswanathan
It is well known that adding side effects to functional languages changes the operational equivalences of the language. We develop a new language construct, encap, that forces imperative pieces of...
Kripke Logical Relations and PCF (1995)
Peter W. O'Hearn, Jon G. Riecke
Sieber has described a model of PCF consisting of continuous functions that are invariant under certain (finitary) logical relations, and shown that it is fully abstract for closed terms of up to...
A Generalization of Exceptions and Control in ML-like Languages (1995)
Carl A. Gunter, Didier Rémy, Jon G. Riecke
We add functional continuations and prompts to a language with an ML-style type system. The operators significantly extend and simplify the control operators in SML/NJ, and can be themselves used to...
Lehman Brothers Corporation (1995)
Jawahar Chirimar, Carl A. Gunter, Jon G. Riecke
We develop formal methods for reasoning about memory usage at a level of abstraction suitable for establishing or refuting claims about the potential applications of linear logic for static analysis....
Delimiting the Scope of Effects (1993)
Program fragments in functional languages may be observationally congruent in a language without effects (continuations, state, exceptions) but not in an extension with effects. We give a generic way...
Statman's 1-Section Theorem (1992)
Statman's 1-Section Theorem [17] is an important but little-known result in the model theory of the simply-typed λ-calculus. The λ-Section Theorem states a necessary and sufficient condition on...
Proving Memory Management Invariants for a Language Based on Linear Logic (1992)
Jawahar Chirimar, Carl A. Gunter, Jon G. Riecke
: We develop tools for the rigorous formulation and proof of properties of runtime memory management for a sample programming language based on a linear type system. Two semantics are described, one...
Algebraic Reasoning and Completeness in Typed Languages (1992)
Jon G. Riecke, Ramesh Subrahmanyam
: We consider the following problem in proving observational congruences in functional languages: given a call-by-name language based on the simplytyped -calculus with algebraic operations...
Proving Memory Management Invariants for a Language Based on Linear Logic (1991)
Chirimar, Jawahar, Gunter, Carl A, Riecke, Jon G
We develop a tool for the rigorous formulation and proof of properties of runtime memory management for a sample programming language based on a linear type system. Two semantics are described, one...
Fully Abstract Translations between Functional Languages (1991)
We examine the problem of finding fully abstract translations between programming languages, i.e., translations that preserve code equivalence and nonequivalence. We present three examples of fully...
The Logic and Expressibility of Simply-typed Call-by-value and Lazy Languages (1991)
Albert R. Meyer, Campbell L. Searle, Jon G. Riecke, Jon Gary Riecke
We study the operational, denotational, and axiomatic semantics of lazy and call-by-value functional languages, and use these semantics to build a new expressiveness theory for comparing functional...
: When observing termination of closed terms at all types in Plotkin's interpreter for PCF [11], the standard cpo model A V is not adequate. We define a new model, A Y , with lifted functional...