Under consideration for publication in J. Functional Programming 1 Persistent Triangulations∗ (2009)
Guy Blelloch, Hal Burch, Karl Crary, Robert Harper, Gary Miller, Noel Walkington
Triangulations of a surface are of fundamental importance in computational geometry, computer graphics, and engineering and scientific simulations. Triangulations are ordinarily represented as...
Programming in Standard ML (WORKING DRAFT OF SEPTEMBER 21, 2008.) (2009)
This book is an introduction to programming with the Standard ML programming language. It began life as a set of lecture notes for Computer Science 15–212: Principles of Programming, the second...
Space Profiling for Parallel Functional Programs (2009)
Daniel Spoonhower, Guy E. Blelloch, Robert Harper, Phillip B. Gibbons
This paper presents a semantic space profiler for parallel functional programs. Building on previous work in sequential profiling, our tools help programmers to relate runtime resource use back to...
Space Profiling for Parallel Functional Programs (2009)
Daniel Spoonhower, Guy E. Blelloch, Robert Harper, Phillip B. Gibbons
This paper presents a semantic space profiler for parallel functional programs. Building on previous work in sequential profiling, our tools help programmers to relate runtime resource use back to...
Focusing on Binding and Computation (2009)
Daniel R. Licata, Noam Zeilberger, Robert Harper
Variable binding is a prevalent feature of the syntax and proof theory of many logical systems. In this paper, we define a programming language that provides intrinsic support for both representing...
Submitted to POPL ’09 Dependently Typed Programming with Domain-Specific Logics (2009)
Daniel R. Licata, Robert Harper
We define a dependent programming language in which programmers can define and compute with domain-specific logics, such as an access-control logic that statically prevents unauthorized access to...
Decidability of definitional equality and conversion of terms into canonical form play a central role in the meta-theory of a type-theoretic logical framework. Most studies of definitional equality...
General Terms Languages, Theory (2009)
Leaf Petersen, Robert Harper, Karl Crary, Frank Pfenning
Abstract Ordered type theory is an extension of linear type theory in whichvariables in the context may be neither dropped nor re-ordered. This restriction gives rise to a natural notion of...
Submitted to PLPV ’09 Positively Dependent Types (2009)
Daniel R. Licata, Robert Harper
This paper is part of a line of work on using the logical techniques of polarity and focusing to design a dependent programming language, with particular emphasis on programming with deductive...
2001, ‘Automatic Generation of Staged Geometric Predicates (2009)
Ar Nanevski, Guy Blelloch, Robert Harper
Abstract. Algorithms in Computational Geometry and Computer Aided Design are often developed for the Real RAM model of computation, which assumes exactness of all the input arguments and operations....
Submitted to POPL ’09 Dependently Typed Programming with Domain-Specific Logics (2009)
Daniel R. Licata, Robert Harper
We define a dependent programming language in which programmers can define and compute with domain-specific logics, such as an access-control logic that statically prevents unauthorized access to...
Typed Compilation of Recursive Datatypes Joseph C. Vanderwaart Derek Dreyer Leaf Petersen (2009)
Karl Crary, Robert Harper, Perry Cheng
1 Introduction The programming language Standard ML (SML) [9] provides a distinctive mechanism for defining recursive types, known as a datatype declaration. For example, the following declaration...
RETROSPECTIVE: TIL: A Type-Directed, Optimizing Compiler for ML (2009)
Robert Harper, Peter Lee, Carnegie Mellon
ABSTRACT The goal of the TIL project was to explore the use of Typed Intermediate Languages to produce high-performance native code from Standard ML (SML). We believed that existing SML compilers...
Robert Harper, Daniel R. Licata
The LF logical framework codifies a methodology for representing deductive systems, such as programming languages and logics, within a dependently typed λ-calculus. In this methodology, the...
General Terms Languages, Theory (2009)
Leaf Petersen, Robert Harper, Karl Crary, Frank Pfenning
Abstract Ordered type theory is an extension of linear type theory in whichvariables in the context may be neither dropped nor re-ordered. This restriction gives rise to a natural notion of...
Typed Compilation of Recursive Datatypes Joseph C. Vanderwaart Derek Dreyer Leaf Petersen (2009)
Karl Crary, Robert Harper, Perry Cheng
1 Introduction The programming language Standard ML (SML) [9] provides a distinctive mechanism for defining recursivetypes, known as a datatype declaration. For example, the following declaration...
Structures General Terms (2009)
Umut A. Acar, Guy E. Blelloch, Robert Harper
We present a framework for applying memoization selectively. The framework provides programmer control over equality, space usage, and identification of precise dependences so that memoization can be...
Abstract Typed Compilation of Recursive Datatypes ∗ (2009)
Joseph C. Vanderwaart, Derek Dreyer, Leaf Petersen, Karl Crary, Robert Harper, Perry Cheng
Standard ML employs an opaque (or generative) semantics of datatypes, in which every datatype declaration produces a new type that is different from any other type, including other identically...
Programming in Standard ML (WORKING DRAFT OF MAY 17, 2005.) (2008)
This book is an introduction to programming with the Standard ML programming language. It began life as a set of lecture notes for Computer Science 15–212: Principles of Programming, the second...
Programming in Standard ML (WORKING DRAFT OF JUNE 25, 2004.) (2008)
This book is an introduction to programming with the Standard ML programming language. It began life as a set of lecture notes for Computer Science 15–212: Principles of Programming, the second...
The Challenges of Clinical e-Science: Lessons Learned (2008)
From Psygrid, John Ainsworth, Robert Harper, Lucy Bridges, Pauline Whelan, William Vance
The PsyGrid project was established to design, build and operate a multi-centre, secure, clinical data capture system that could support clinical trials and cohort studies from any clinical domain....
Programming in Standard ML (WORKING DRAFT OF DECEMBER 9, 2002.) (2008)
This book is an introduction to programming with the Standard ML programming language. It began life as a set of lecture notes for Computer Science 15–212: Principles of Programming, the second...
I. TAX EXEMPT ORGANIZATIONS AND WORLD WIDE WEB FUNDRAISING AND ADVERTISING ON THE INTERNET (2008)
Cheryl Chasin, Susan Ruth, Robert Harper
The purpose of this article is to discuss solicitation of contributions, advertising, and merchandising techniques under the Internet’s World Wide Web (WWW) protocol by taxexempt organizations....
Selective Memoization \Lambda (2008)
Umut A. Acar, Guy E. Blelloch, Robert Harper
Abstract We present a framework for applying memoization selectively. The framework provides programmer control over equality, space usage, and identification of precise dependences so that...
ML modules and Haskell type classes have proven to be highly effective tools for program structuring. Modules emphasize explicit configuration of program components and the use of data abstraction....
www.elsevier.com/locate/entcs A Library for Self-Adjusting Computation (2008)
Umut Acar, Guy Blelloch, Matthias Blume, Robert Harper, Kanat Tangwongsan
We present a Standard ML library for writing programs that automatically adjust to changes to their data. The library combines modifiable references and memoization to achieve efficient updates. We...
Programming in Standard ML (WORKING DRAFT OF MARCH 25, 2001.) (2008)
This book is an introduction to programming with the Standard ML programming language. It began life as a set of lecture notes for Computer Science 15–212: Principles of Programming, the second...
Programming in Standard ML (WORKING DRAFT OF DECEMBER 6, 2007.) (2008)
This book is an introduction to programming with the Standard ML programming language. It began life as a set of lecture notes for Computer Science 15–212: Principles of Programming, the second...
Programming in Standard ML (WORKING DRAFT OF NOVEMBER 3, 2004.) (2008)
This book is an introduction to programming with the Standard ML programming language. It began life as a set of lecture notes for Computer Science 15–212: Principles of Programming, the second...
Programming in Standard ML (WORKING DRAFT OF APRIL 23, 2007.) (2008)
This book is an introduction to programming with the Standard ML programming language. It began life as a set of lecture notes for Computer Science 15–212: Principles of Programming, the second...
Completely annotated lambda terms (such as are arrived at via the straightforward encodings of various types from System F) contain much redundant type information. Consequently, the completely...
Daniel Spoonhower, Guy Blelloch, Robert Harper
We introduce an extension of mostly copying collection that uses page residency to determine when to relocate objects. Our collector promotes pages with high residency in place, avoiding unnecessary...
Focusing on Computation with Binding (2008)
Daniel R. Licata, Noam Zeilberger, Robert Harper
Abstract—Variable binding is a prevalent feature of the syntax and proof theory of many logical systems. In this paper, we define a programming language that provides intrinsic support for both...
Abstract Adaptive Memoization ∗ (2008)
Umut A. Acar, Guy E. Blelloch, Robert Harper
Memoization may be reviewed as a mechanism for re-using a computation—if a function is re-applied to the same argument we may re-use the previous computation to determine the result, rather than...
Mechanizing a Decision Procedure for Coproduct Equality (2008)
Arbob Ahmad, Daniel R. Licata, Robert Harper
In many applications of λ-calculi, it is essential to compare λ-terms for equality. For example, type checking a dependently typed programming language requires deciding equality of its terms and...
Compliance with Methodological Standards When Evaluating Ophthalmic Diagnostic Tests (2008)
PURPOSE. To draw attention to the importance of methodological standards when carrying out evaluations of ophthalmic diagnostic tests by reviewing the extent of compliance with these standards in...
Robert Harper, Daniel R. Licata
The LF logical framework codifies a methodology for representing deductive systems, such as programming languages and logics, within a dependently typed λ-calculus. In this methodology, the...
Extensional equivalence and singleton types (2008)
Christopher A. Stone, Robert Harper
We study the λΠΣS ≤ calculus, which contains singleton types S(M) classifying terms of base type provably equivalent to the term M. The system includes dependent types for pairs and functions...
Daniel Spoonhower, Guy Blelloch, Robert Harper
We introduce an extension of mostly copying collection that uses page residency to determine when to relocate objects. Our collector promotes pages with high residency in place, avoiding unnecessary...
ABSTRACT An Effective Theory of Type Refinements (2008)
Yitzhak Mandelbaum, David Walker, Robert Harper
We develop an explicit two level system that allows programmers to reason about the behavior of effectful programs. The first level is an ordinary ML-style type system, which confers standard...
ML 2005 Preliminary Version A Library for Self-Adjusting Computation Abstract (2008)
Umut Acar, Guy Blelloch, Matthias Blume, Robert Harper, Kanat Tangwongsan
We present a Standard ML library for writing programs that automatically adjust to changes to their data. The library combines modifiable references and memoization to achieve efficient updates. We...
On the unusual effectiveness of Logic in computer science (2008)
Joseph Y. Halpern, Robert Harper, Neil Immerman, Phokion G. Kolaitis, Moshe Y. Vardi, Victor Vianu
Type Systems for Programming Languages 1 (DRAFT) (2008)
This is an incomplete, working draft, not intended for publication. Citations to the literature are spotty at best; no results presented here should be considered original unless explicitly stated...
Corrigendum: Polymorphic Type Assignment and CPS Conversion (2008)
Robert Harper, Mark Lillibridge
It has come to our attention that there is an error in the proof of Theorem 6 on page 373 of the above titled paper [1]. Specifically, the term e ′ 0 does not type check in the system named DM as...
ABSTRACT An Effective Theory of Type Refinements (2008)
Yitzhak Mandelbaum, David Walker, Robert Harper
We develop an explicit two level system that allows programmers to reason about the behavior of effectful programs. The first level is an ordinary ML-style type system, which confers standard...
Umut A. Acar, Guy E. Blelloch, Robert Harper
We present techniques for incremental computing by introducing adaptive functional programming. As an adaptive program executes, the underlying system represents the data and control dependences in...
Abstract A Type System for Higher-Order Modules (2008)
Derek Dreyer, Karl Crary, Robert Harper
We present a type theory for higher-order modules that accounts for most current issues in modular programming languages, including translucency, applicativity, generativity, and modules as...
On the unusual effectiveness of Logic in computer science (2008)
Joseph Y. Halpern, Robert Harper, Moshe Y. Vardi, Neil Immerman
The method of logical relations assigns a relational interpretation to types that expresses operational invariants satisfied by all terms of a type. The method is widely used in the study of typed...
Towards a Functional Library for Fault-Tolerant Grid Computing ⋆ (2008)
Margaret Delap, Jason Liszka, Tom Murphy Vii, Karl Crary, Robert Harper, ...
Abstract. To make development of grid applications less arduous, a natural, powerful, and convenient programming interface is required. First, we propose an expressive grid programming language which...
Edinburgh EH9-3JZ, U.K. Abstract (2008)
Robert Harper, Eugenio Moggi, John C. Mitchell
Typed λ-calculus is an important tool in programming language research because it provides an extensible framework for studying language features both in isolation and in their relation to each...
Abstract Abstract Models of Memory Management (2008)
Greg Morrisett, Matthias Felleisen, Robert Harper
Most speci cations of garbage collectors concentrate on the low-level algorithmic details of how to nd and preserve accessible objects. Often, they focus on bit-level manipulations such as \scanning...
Type-safe distributed programming with ML5 (2008)
Tom Murphy Vii, Karl Crary, Robert Harper
Abstract We present ML5, a high level programming language for spatially distributed computing. The language, a variant of ML, allows an entire distributed application to be developed and reasoned...
The method of logical relations assigns a relational interpretation to types that expresses operational invariants satisfied by all terms of a type. The method is widely used in the study of typed...
General Terms Languages, Theory (2008)
Derek Dreyer, Karl Crary, Robert Harper
Abstract We present a type theory for higher-order modules that accountsfor many central issues in module system design, including translucency, applicativity, generativity, and modules as...
Abstract Mechanizing the Metatheory of Standard ML ∗ (2008)
Daniel K. Lee, Karl Crary, Robert Harper
We present an internal language with equivalent expressive power to Standard ML, and discuss its formalization in LF and the machine-checked verification of its type safety in Twelf. The internal...
Robert Harper, Daniel R. Licata
The LF logical framework codifies a methodology for representing deductive systems, such as programming languages and logics, within a dependently typed λ-calculus. In this methodology, the...
Memory management General Terms (2008)
Leaf Petersen, Robert Harper, Karl Crary, Frank Pfenning
Ordered type theory is an extension of linear type theory in which variables in the context may be neither dropped nor re-ordered. This restriction gives rise to a natural notion of adjacency. We...
Memory management General Terms (2008)
Leaf Petersen, Robert Harper, Karl Crary, Frank Pfenning
Ordered type theory is an extension of linear type theory in which variables in the context may be neither dropped nor re-ordered. This restriction gives rise to a natural notion of adjacency. We...
Programming in Standard ML (WORKING DRAFT OF DECEMBER 6, 2007.) (2008)
This book is an introduction to programming with the Standard ML programming language. It began life as a set of lecture notes for Computer Science 15–212: Principles of Programming, the second...
Towards a Functional Library for Fault-Tolerant Grid Computing ⋆ (2008)
Margaret Delap, Jason Liszka, Tom Murphy Vii, Karl Crary, Robert Harper, ...
Abstract. To make development of grid applications less arduous, a natural, powerful, and convenient programming interface is required. First, we propose an expressive grid programming language which...
A Semantic Framework for Scheduling Parallel Programs (2008)
Daniel Spoonhower, Guy E. Blelloch, Robert Harper
Abstract. Declarative parallel programs offer deterministic results, allowing the language implementation to schedule parallel tasks in any order. However, program performance hinges crucially on the...
Decidability of definitional equality and conversion of terms into canonical form play a central role in the meta-theory of a type-theoretic logical framework. Most studies of definitional equality...
Type-safe distributed programming with ML5 (2008)
Tom Murphy Vii, Karl Crary, Robert Harper
Abstract We present ML5, a high level programming language for spatially distributed computing. The language, a variant of ML, allows an entire distributed application to be developed and reasoned...
Andrew Bernard, Robert Harper, Peter Lee
Abstract. We describe the integration of MLRISC, a \generic " compiler back end, with TIL, a type-directed compiler for Standard ML. The TIL run-time system uses a form of type information...
Abstract Typed Compilation of Recursive Datatypes ∗ (2008)
Joseph C. Vanderwaart, Derek Dreyer, Leaf Petersen, Karl Crary, Robert Harper, Perry Cheng
Standard ML employs an opaque (or generative) semantics of datatypes, in which every datatype declaration produces a new type that is different from any other type, including other identically...
Towards a Functional Library for Fault-Tolerant Grid Computing ⋆ (2008)
Margaret Delap, Jason Liszka, Tom Murphy Vii, Karl Crary, Robert Harper, ...
Abstract. To make development of grid applications less arduous, a natural, powerful, and convenient programming interface is required. First, we propose an expressive grid programming language which...
Towards a Functional Library for Fault-Tolerant Grid Computing ⋆ (2008)
Margaret Delap, Jason Liszka, Tom Murphy Vii, Karl Crary, Robert Harper, ...
Abstract. To make development of grid applications less arduous, a natural, powerful, and convenient programming interface is required. First, we propose an expressive grid programming language which...
Abstract Adaptive Memoization ∗ (2008)
Umut A. Acar, Guy E. Blelloch, Robert Harper
Memoization may be viewed as a mechanism for re-using a computation—if a function is re-applied to the same argument we may re-use the previous computation to determine the result, rather than...
Abstract Typed Closure Conversion for Recursively-De ned Functions (Extended Abstract) (2008)
Much recent work on the compilation of statically typed languages such asMLrelies on the propagation of type information from source to object code in order to increase the reliability and...
Parametricity and variants of Girard's J operator (2008)
Robert Harper, John C. Mitchell
The Girard-Reynolds polymorphic-calculus is generally regarded as a calculus of parametric polymorphism in which all well-formed terms are strongly normalizing with respect to-reductions. Girard...
Under consideration for publication in J. Functional Programming 1 Persistent Triangulations∗ (2008)
Guy Blelloch, Hal Burch, Karl Crary, Robert Harper, Gary Miller, Noel Walkington
Triangulations of a surface are of fundamental importance in computational geometry, computer graphics, and engineering and scientific simulations. Triangulations are ordinarily represented as...
A Logical View of Effects (2008)
Despite their invaluable contribution to the programming language community, monads as a foundation for the study of effects have three problems: they make it difficult to combine effects; they...
Robert Harper Computer, Karl Crary, Robert Harper
The method of logical relations assigns a relational interpretation to types that expresses operational invariants satisfied by all terms of a type. The method is widely used in the study of typed...
Self-Adjusting Programming (2008)
Umut Acar Guy, Guy E. Blelloch, Matthias Blume, Robert Harper
This papers proposes techniques for writing self-adjusting programs that can adjust to any change to their data (e.g., inputs, decisions made during the computation) etc. We show that the techniques...
Strict Bidirectional Type Checking (2008)
Adam Chlipala Computer, Adam Chlipala, Robert Harper
Completely annotated lambda terms (such as are arrived at via the straightforward encodings of various types from System F) contain much redundant type information. Consequently, the completely...
Using Page Residency to Balance Tradeoffs (2008)
In Tracing Garbage, Daniel Spoonhower, Guy Blelloch, Robert Harper
We introduce an extension of mostly copying collection that uses page residency to determine when to relocate objects. Our collector promotes in place pages with high residency, avoiding unnecessary...
Distributed Control Flow (2008)
With Classical Modal, Tom Murphy Vii, Karl Crary, Robert Harper
In previous work we presented a foundational calculus for spatially distributed computing based on intuitionistic modal logic. With the modalities # and # we were able to capture two key invariants:...
This is a working draft of a book on the foundations of programming languages. The central organizing principle of the book is that programming language features may be seen as manifestations of an...
Focusing on Binding and Computation (2008)
Daniel R. Licata, Noam Zeilberger, Robert Harper
Variable binding is a prevalent feature of the syntax and proof theory of many logical systems. In this paper, we define a programming language that provides intrinsic support for both representing...
Focusing on Binding and Computation (2008)
Daniel R. Licata, Noam Zeilberger, Robert Harper
Variable binding is a prevalent feature of the syntax and proof theory of many logical systems. In this paper, we define a programming language that provides intrinsic support for both representing...
Space Profiling for Parallel Functional Programs (2008)
Daniel Spoonhower, Guy E. Blelloch, Phillip B. Gibbons, Robert Harper
This paper presents a semantic space profiler for parallel functional programs. Building on previous work in sequential profiling, our tools help programmers to relate runtime resource use back to...
Focusing on binding and computation (2008)
Daniel R. Licata, Noam Zeilberger, Robert Harper
Variable binding is a prevalent feature of the syntax and proof theory of many logical systems. In this paper, we define a programming language that provides intrinsic support for both representing...
Programming in Standard ML (WORKING DRAFT OF OCTOBER 26, 2000.) (2007)
These notes are intended as a brief introduction to Standard ML (1997 dialect) for the experienced programmer. They began as lecture notes for 15– 212: Principles of Programming, the second...
Fred B. Schneider, Greg Morrisett, Robert Harper
Abstract. Language-based security leverages program analysis and program rewriting to enforce security policies. The approach promises e-cient enforcement of ne-grained access control policies and...
Programming in Standard ML (WORKING DRAFT OF OCTOBER 26, 2000.) (2007)
These notes are intended as a brief introduction to Standard ML (1997 dialect) for the experienced programmer. They began as lecture notes for 15– 212: Principles of Programming, the second...
Programming in Standard ML (WORKING DRAFT OF JANUARY 8, 2001.) (2007)
This book is an introduction to programming with the Standard ML programming language. It began life as a set of lecture notes for Computer Science 15–212: Principles of Programming, the second...
Programming in Standard ML (WORKING DRAFT OF JANUARY 8, 2001.) (2007)
This book is an introduction to programming with the Standard ML programming language. It began life as a set of lecture notes for Computer Science 15–212: Principles of Programming, the second...
Joseph Y. Halpern, Robert Harper, Neil Immerman, Phokion G. Kolaitis, Moshe Y. Vardi
k Victor Vianu
Joseph Y. Halpern, Robert Harper, Neil Immerman, Phokion G. Kolaitis, Moshe Y. Vardi
k Victor Vianu
Computer Science 15-312 Computational Eects (2007)
Robert Harper Spring, Robert Harper
Introduction MinML is a purely functional language, in two senses. First, the only control mechanism is procedure call and return. Procedures may call themselves recursively, which is the sole means...
Computer Science 15-312 Computational Eects (2007)
Robert Harper Spring, Robert Harper
Introduction MinML is a purely functional language, in two senses. First, the only control mechanism is procedure call and return. Procedures may call themselves recursively, which is the sole means...
Compiling with Non-Parametric Polymorphism (Preliminary Report) (2007)
There is a middle ground between parametric and ad-hoc polymorphism in which a computation can depend upon a type parameter but is restricted to being defined at all types in an inductive fashion. We...
Derek Dreyer, Karl Crary, Robert Harper
We present a type theory for higher-order modules that accounts for many central issues in module system design, including translucency, applicativity, generativity, and modules as first-class...
Carnegie-Mellon University and (2007)
Robert Harper, John C. Mitchell
Standard ML is a useful programming language with a polymorphic type system and a flexible module facility. One notable feature of the core expression language of ML is that it is implicdy typed: no...
On Equivalence and Canonical Forms in the LF Type Theory (Extended Abstract) (2007)
Decidability of definitional equality and conversion of terms into canonical form play a central role in the meta-theory of a type-theoretic logical framework. Most studies of definitional equality...
Towards a Functional Library for Fault-Tolerant Grid Computing (2007)
Margaret Delap, Jason Liszka, Tom Murphy Vii, Karl Crary, Robert Harper, ...
Abstract. To make development of grid applications less arduous, a natural, powerful, and convenient programming interface is required. First, we propose an expressive grid programming language which...
Towards a Functional Library for Fault-Tolerant Grid Computing (2007)
Margaret Delap, Jason Liszka, Tom Murphy Vii, Karl Crary, Robert Harper, ...
Abstract. To make development of grid applications less arduous, a natural, powerful, and convenient programming interface is required. First, we propose an expressive grid programming language which...
FUNCTIONAL PEARLS Proof-Directed Debugging (2007)
The close relationship between writing programs and proving theorems has frequently been cited as an advantage of functional programming languages. We illustrate the interplay between programming and...
Fred B. Schneider, Greg Morrisett, Robert Harper
Abstract. Language-based security leverages program analysis and program rewriting to enforce security policies. The approach promises e#-cient enforcement of fine-grained access control policies and...
Karl Crary, Robert Harper, Peter Lee, Frank Pfenning
We contend that modularity is the key to improving software quality. We advocate a view of modularity that emphasizes not the mere assembling of software systems from component parts, but rather the...
Robert Harper, Bruce F. Duba, David Macqueen
An extension of ML with continuation primitives similar to those found in Scheme is considered. A number of alternative type systems are discussed, and several programming examples are given. A...
Programming in Standard ML (WORKING DRAFT OF JUNE 28, 2001.) (2007)
This book is an introduction to programming with the Standard ML programming language. It began life as a set of lecture notes for Computer Science 15–212: Principles of Programming, the second...
Programming in Standard ML (WORKING DRAFT OF MARCH 25, 2001.) (2007)
This book is an introduction to programming with the Standard ML programming language. It began life as a set of lecture notes for Computer Science 15–212: Principles of Programming, the second...
Under consideration for publication in J. Functional Programming 1 Persistent Triangulations∗ (2007)
Guy Blelloch, Hal Burch, Karl Crary, Robert Harper, Gary Miller, Noel Walkington
Triangulations of a surface are of fundamental importance in computational geometry, computer graphics, and engineering and scientific simulations. Triangulations are ordinarily represented as...
Joseph Y. Halpern, Robert Harper, Neil Immerman, Phokion G. Kolaitis, Moshe Y. Vardi
k Victor Vianu
Programming in Standard ML (WORKING DRAFT OF DECEMBER 19, 2000.) (2007)
This book is an introduction to programming with the Standard ML programming language. It began life as a set of lecture notes for Computer Science 15–212: Principles of Programming, the second...
Programming in Standard ML (WORKING DRAFT OF DECEMBER 19, 2000.) (2007)
This book is an introduction to programming with the Standard ML programming language. It began life as a set of lecture notes for Computer Science 15–212: Principles of Programming, the second...
Projects Agency or the U.S. Government. (2007)
Robert Harper, Mark Lillibridge
Meyer and Wand established that the type of a term in the simply typed-calculus may be related in a straightforward manner to the type of its call-by-value CPS transform. This typing property may be...
Programming in Standard ML (2007)
These notes are intended as a brief introduction to Standard ML (1997 dialect) for the experienced programmer. They began as lecture notes for 15-212: Fundamental Principles of Computer Science II,...
Efficient Recursion in the Presence of Effects (2007)
Derek Dreyer, Robert Harper, Karl Crary
In the interest of designing a recursive module extension to ML that is as simple and general as possible, we study the important subproblem of how to support recursive definitions of effectful...
Umut A. Acar, Guy E. Blelloch, Robert Harper
Memoization may be viewed as a mechanism for re-using a computation---if a function is re-applied to the same argument we may re-use the previous computation to determine the result, rather than...
A Symmetric Modal Lambda Calculus for Distributed Computing # (2007)
Tom Murphy Vii, Karl Crary, Robert Harper, Frank Pfenning
We present a foundational language for distributed programming, called Lambda 5, that addresses both mobility of code and locality of resources. In order to construct our system, we appeal to the...
Extensional equivalence and singleton types (2007)
Christopher A. Stone, Robert Harper
In this paper we study a λ-calculus enriched with singleton types, where the type S(M) classifies all terms of base type provably equivalent to the term M. We also have dependent types for pairs and...
ABSTRACT An Effective Theory of Type Refinements (2007)
Yitzhak Mandelbaum, David Walker, Robert Harper
We develop an explicit two level system that allows programmers to reason about the behavior of effectful programs. The first level is an ordinary ML-style type system, which confers standard...
A Symmetric Modal Lambda Calculus for Distributed Computing # (2007)
Tom Murphy Vii, Karl Crary, Robert Harper, Frank Pfenning
We present a foundational language for spatially distributed programming, called Lambda 5, that addresses both mobility of code and locality of resources. In order to construct our system, we appeal...
Abstract. Algorithms in Computational Geometry and Computer Aided Design are often developed for the Real RAM model of computation, which assumes exactness of all the input arguments and operations....
Despite many concentrated research efforts in various areas such as software engineering, programming languages, and logic, software today is not fundamentally more reliable than it was a decade ago....
Toward a Practical Type Theory for Recursive Modules (2007)
Dreyer, Derek R., Harper, Robert, Crary, Karl
Module systems for languages with complex type systems, such as Standard ML, often lack the ability to express mutually recursive type and function dependencies across module boundaries. Previous...
A language for access control (2007)
We present a language for access control. The language is organized around the notion of execution on behalf of a principal. This is characterized using an indexed lax modality. Central to the...
A Unified System of Type Refinements (2007)
Joshua Dunfield, Jonathan Aldrich, Robert Harper
through a generous student fellowship from the NSF. The views and conclusions contained in this document are those
Thesis Proposal: The logical basis of evaluation order (2007)
Noam Zeilberger, Peter Lee, Robert Harper, Paul-andré Melliès
Most type systems are agnostic regarding the evaluation strategy for the underlying languages, with the value restriction for ML which is absent in Haskell as a notable exception. As type systems...
Project Summary Manifest Security (2007)
Karl Crary, Robert Harper, Frank Pfenning, Benjamin C. Pierce, Stephanie Weirich, Stephan Zdancewic
This project proposes manifest security as a new architectural principle for secure extensible systems. Its research objectives are to develop the theoretical foundations for manifestly secure...
Project Summary Manifest Security (2007)
Karl Crary, Robert Harper, Frank Pfenning, Benjamin C. Pierce, Stephanie Weirich, Stephan Zdancewic
This project proposes manifest security as a new architectural principle for secure extensible systems. Its research objectives are to develop the theoretical foundations for manifestly secure...
Project Summary Manifest Security (2007)
Karl Crary, Robert Harper, Frank Pfenning, Benjamin C. Pierce, Stephanie Weirich, Stephan Zdancewic
This project proposes manifest security as a new architectural principle for secure extensible systems. Its research objectives are to develop the theoretical foundations for manifestly secure...
Logic Column 16: Higher-Order Abstract Syntax: Setting the Record Straight (2006)
This article responds to a critique of higher-order abstract syntax appearing in Logic Column 14, ``Nominal Logic and Abstract Syntax'', cs.LO/0511025.
A Type-Theoretic Approach to Higher-Order Modules with Sharing (2006)
Harper, Robert, Lillibridge, Mark
The design of a module system for constructing and maintaining large programs is a difficult task that at raises a number of theoretical and practical issues. A fundamental issue is the management of...
Compiling Polymorphism Using Intensional Type Analysis (2006)
Harper, Robert, Morrisett, Greg
Types have been used to describe the size and shape of data structures at compile time. In polymorphic languages or languages with abstract types, this is not possible since the types of some objects...
Advanced Languages for Systems Software (2006)
It has been amply demonstrated in recent years that careful attention to the structure of systems software can lead to greater flexibility, reliability, and ease of implementation, without incurring...
A Separate Compilation Extension to Standard ML (Revised and Expanded) (2006)
Swasey, David, Crary, Karl, Harper, Robert
We present an extension to Standard ML, called SMLSC, to support separate compilation. The system gives meaning to individual program fragments, called units. Units may depend on one another in a way...
Manifest Security for Distributed Information (2006)
Karl Crary, Robert Harper, Frank Pfenning, Benjamin C. Pierce, Stephanie Weirich, Stephan Zdancewic
What is the best way to build programs that compute with data sources controlled by multiple principals, while ensuring compliance with the security policies of the principals involved? The objective...
A separate compilation extension to Standard ML (revised and expanded (2006)
David Swasey, Tom Murphy, Vii Karl Crary, Robert Harper
Introduction We propose an extension to Standard ML called SMLSC. SMLSC supports separate compilation in the sense that it gives a static semantics to individual program fragments, which we call...
Mechanizing Language Definitions (2006)
Robert Harper, Daniel R. Licata
We present a technical introduction to mechanizing language definitions and meta-theory using LF and Twelf. LF is a logical framework designed for representing languages that are specified by...
The Cult of the Bound Variable: (2006)
The Annual Icfp, Tom Murphy, Vii Daniel, Spoonhower Chris, Casinghino Daniel, R. Licata, ...
The annual ICFP Programming Contest has become one of the premiere programming competitions in the world. The 9 incarnation of the contest, "The Cult of the Bound Variable," was held in...
A Separate Compilation Extension to Standard ML (2006)
Revised And Expanded, David Swasey, Tom Murphy, Vii Karl Crary, Robert Harper
We present an extension to Standard ML, called SMLSC, to support separate compilation. The system gives meaning to individual program fragments, called units. Units may depend on one another in a way...
Mechanizing the Metatheory of Standard ML (2006)
Daniel K. Lee, Karl Crary, Robert Harper
We present an internal language with equivalent expressive power to Standard ML, and discuss its formalization in LF and the machine-checked verification of its type safety in Twelf. The internal...
Manifest Security for Distributed Information (2006)
Karl Crary, Robert Harper, Frank Pfenning, Benjamin C. Pierce, Stephanie Weirich, Stephan Zdancewic
gical methods for specifying and verifying them. These properties will be formally verified against precise specifications written in a novel logic of authorization and information flow using...
Manifest Security for Distributed Information (2006)
Karl Crary, Robert Harper, Frank Pfenning, Benjamin C. Pierce, Stephanie Weirich, Stephan Zdancewic
al methods for specifying and verifying them. These properties will be formally verified against precise specifications written in a novel logic of authorization and information flow using mechanized...
The cult of the bound variable: The 9 th annual ICFP programming contest (2006)
Tom Murphy, Vii Daniel, Spoonhower Chris Casinghino, Daniel R. Licata, Karl Crary, Robert Harper
The annual ICFP Programming Contest has become one of the premiere programming competitions in the world. The 9 th incarnation of the contest, “The Cult of the Bound Variable, ” was held in July...
Manifest Security for Distributed Information (2006)
Karl Crary, Robert Harper, Frank Pfenning, Benjamin C. Pierce, Stephanie Weirich, Stephan Zdancewic
What is the best way to build programs that compute with data sources controlled by multiple principals, while ensuring compliance with the security policies of the principals involved? The objective...
A separate compilation extension to Standard ML (working draft (2006)
David Swasey, Tom Murphy, Vii Karl Crary, Robert Harper
This is a proposal for an extension to the Standard ML programming language to support separate compilation. The extension allows the programmer to write a program broken into multiple fragments in a...
Manifest Security for Distributed Information (2006)
Karl Crary, Robert Harper, Frank Pfenning, Benjamin C. Pierce, Stephanie Weirich, Stephan Zdancewic
A separate compilation extension to Standard ML (working draft (2006)
David Swasey, Tom Murphy, Vii Karl Crary, Robert Harper
This is a proposal for an extension to the Standard ML programming language to support separate compilation. The extension allows the programmer to write a program broken into multiple fragments in a...
A separate compilation extension to Standard ML (revised and expanded (2006)
David Swasey, Tom Murphy, Vii Karl Crary, Robert Harper
We present an extension to Standard ML, called SMLSC, to support separate compilation. The system gives meaning to individual program fragments, called units. Units may depend on one another in a way...
An experimental analysis of self-adjusting computation (2006)
Umut A. Acar, Guy E. Blelloch, Matthias Blume, Robert Harper
Self-adjusting computation uses a combination of dynamic dependence graphs and memoization to efficiently update the output of a program as the input changes incrementally or dynamically over time....
References Type Systems as a Foundation for Reliable Computing (2005)
These lectures are based on the course Constructive Logic at Carnegie Mellon University. The course materials are available at the course web site:
Distributed Control Flow with Classical Modal Logic (2005)
Tom Murphy VII, Karl Crary, Robert Harper, Tom Murphy, Vii Karl, Crary Robert Harper
In previous work we presented a foundational calculus for spatially distributed computing based on intuitionistic modal logic. Through the modalities # and # we were able to capture two key...
A Programming Language for Probabilistic Computation (2005)
Sungwoo Park, Geoffrey Gordon, Robert Harper
As probabilistic computations play an increasing role in solving various problems, researchers have designed probabilistic languages to facilitate their modeling. Most of the existing probabilistic...
A Formulation of Dependent ML with Explicit Equality Proofs (2005)
Daniel R. Licata, Robert Harper
We study a calculus that supports dependent programming in the style of Xi and Pfenning's Dependent ML. Xi and Pfenning's language determines equality of static data using a built-in...
Practical Refinement-Type Checking (2005)
Rowan Davies, Robert Harper, Peter Lee, John Reynolds
Software development is a complex and error prone task. Programming languages with strong static type systems assist programmers by capturing and checking the fundamental structure of programs in a...
A Formulation of Dependent ML with Explicit Equality Proofs (2005)
Daniel R. Licata, Robert Harper
We study a calculus that supports dependent programming in the style of Xi and Pfenning's Dependent ML. Xi and Pfenning's language determines equality of static data using a built-in...
Distributed Control Flow (2005)
With Classical Modal, Tom Murphy Vii, Karl Crary, Robert Harper
In previous work we presented a foundational calculus for spatially distributed computing based on intuitionistic modal logic. With the modalities # and # we were able to capture two key invariants:...
A Programming Language for Probabilistic Computation (2005)
Sungwoo Park, Geoffrey Gordon, Robert Harper
F1962895C0050 and F306029820137, the US Army under contract no. DABT6300C1016, and through a generous grant from the National Science Foundation. The views and conclusions contained in this document...
A formulation of Dependent ML with explicit equality proofs (2005)
Daniel R. Licata, Robert Harper
We study a calculus that supports dependent programming in the style of Xi and Pfenning’s Dependent ML. Xi and Pfenning’s language determines equality of static data using a built-in decision...
Distributed control flow with classical modal logic (2005)
Tom Murphy, Vii Karl Crary, Robert Harper
In previous work we presented a foundational calculus for spatially distributed computing based on intuitionistic modal logic. Through the modalities ✷ and ✸ we were able to capture two key...
A network protocol stack in Standard ML. Higher Order Symbol (2004)
Edoardo Biagioni, Robert Harper, Peter Lee
The FoxNet is an implementation of the standard TCP/IP networking protocol stack using the Standard ML (SML) language. SML is a type-safe (no type casts allowed) programming language with garbage...
A Symmetric Modal Lambda Calculus for Distributed Computing (2004)
Tom Murphy VII, Karl Crary, Robert Harper, Tom Murphy, Vii Karl, Crary Robert Harper, ...
We present a foundational language for distributed programming, called Lambda 5, that addresses both mobility of code and locality of resources. In order to construct our system, we appeal to the...
A Symmetric Modal Lambda Calculus for Distributed Computing (2004)
Tom Murphy VII, Karl Crary, Robert Harper, Tom Murphy, Vii Karl, Crary Robert Harper, ...
We present a foundational language for distributed programming, called Lambda 5, that addresses both mobility of code and locality of resources. In order to construct our system, we appeal to the...
A Symmetric Modal Lambda Calculus for Distributed Computing (2004)
Tom Murphy VII, Karl Crary, Robert Harper, Tom Murphy, Vii Karl, Crary Robert Harper, ...
We present a foundational language for distributed programming, called Lambda 5, that addresses both mobility of code and locality of resources. In order to construct our system, we appeal to the...
Umut A. Acar, Guy E. Blelloch, Robert Harper
We combine adaptivity and memoization to obtain an incremental computation technique that dramatically improves performance over adaptivity and memoization alone. The key contribution is adaptive...
Dynamizing Static Algorithms, with Applications to Dynamic Trees and History Independence (2004)
Umut A. Acar, Guy E. Blelloch, Robert Harper, Jorge L. Vittes, Shan Leung
We describe a machine model for automatically dynamizing static algorithms and apply it to historyindependent data structures. Static programs expressed in this model are dynamized automatically by...
A type system for well-founded recursion (2004)
Derek Dreyer, Robert Harper, Karl Crary
In the interest of designing a recursive module extension to ML that is as simple and general as possible, we propose a novel type system for general recursion over effectful expressions. The...
A network protocol stack in Standard ML. Higher Order Symbol (2004)
Edoardo Biagioni, Robert Harper, Peter Lee
Abstract. The FoxNet is an implementation of the standard TCP/IP networking protocol stack using the Standard ML (SML) language. SML is a type-safe programming language with garbage collection, a...
A network protocol stack in Standard ML. Higher Order Symbol (2004)
Edoardo Biagioni, Robert Harper, Peter Lee
Abstract. The FoxNet is an implementation of the standard TCP/IP networking protocol stack using the Standard ML (SML) language. SML is a type-safe programming language with garbage collection, a...
Types for Systems Design: A Position Paper (2003)
There is a enormous gulf between the design principles governing a software system and its implementation. Designs are expressed in many forms, from blackboard drawings, informal analogoies,...
A type theory for memory allocation and data layout (2003)
Leaf Petersen, Robert Harper, Karl Crary, Frank Pfenning
Ordered type theory is an extension of linear type theory in which variables in the context may be neither dropped nor re-ordered. This restriction gives rise to a natural notion of adjacency. We...
Typed compilation of recursive datatypes (2003)
Joseph C. Vanderwaart, Derek Dreyer, Leaf Petersen, Karl Crary, Robert Harper, Perry Cheng
Standard ML employs an opaque (or generative) semantics of datatypes, in which every datatype declaration produces a new type that is different from any other type, including other identically...
Typed compilation of recursive datatypes (2003)
Joseph C. Vanderwaart, Derek Dreyer, Leaf Petersen, Karl Crary, Robert Harper, Perry Cheng
Standard ML employs an opaque (or generative) semantics of datatypes, in which every datatype declaration produces a new type that is different from any other type, including other identically...
A type theory for memory allocation and data layout (2003)
Leaf Petersen, Robert Harper, Karl Crary, Frank Pfenning
Ordered type theory is an extension of linear type theory in which variables in the context may be neither dropped nor re-ordered. This restriction gives rise to a natural notion of adjacency. We...
A type theory for memory allocation and data layout (2003)
Leaf Petersen, Robert Harper, Karl Crary, Frank Pfenning
Ordered type theory is an extension of linear type theory in which variables in the context may be neither dropped nor re-ordered. This restriction gives rise to a natural notion of adjacency. We...
A type theory for memory allocation and data layout (2003)
Leaf Petersen, Robert Harper, Karl Crary, Frank Pfenning
Ordered type theory is an extension of linear type theory in which variables in the context may be neither dropped nor re-ordered. This restriction gives rise to a natural notion of adjacency. We...
Umut A. Acar, Guy E. Blelloch, Robert Harper
We present a framework for applying memoization selectively. The framework provides programmer control over equality, space usage, and identification of precise dependences so that memoization can be...
A type theory for memory allocation and data layout (2003)
Leaf Petersen, Robert Harper, Karl Crary, Frank Pfenning
Ordered type theory is an extension of linear type theory in which variables in the context may be neither dropped nor re-ordered. This restriction gives rise to a natural notion of adjacency. We...
A type system for higher-order modules (2003)
Karl Crary, Robert Harper, Derek Dreyer
We present a type theory for higher-order modules that accounts for most current issues in modular programming languages, including translucency, applicativity, generativity, and modules as rst-class...
Umut A. Acar, Guy E. Blelloch, Robert Harper
We combine adaptivity and memoization to obtain an incremental computation technique that dramatically improves performance over adaptivity and memoization alone. The key contribution is adaptive...
Umut A. Acar, Guy E. Blelloch, Robert Harper
We present a framework for applying memoization selectively. The framework provides programmer control over equality, space usage, and identification of precise dependences so that memoization can be...
Umut Acar Guy, Guy E. Blelloch, Robert Harper
We present a framework for applying memoization selectively. The framework provides programmer control over equality, space usage, and identification of precise dependences so that memoization can be...
A Type Theory for Memory Allocation and Data (2003)
Layout Extended Version, Leaf Petersen, Robert Harper, Karl Crary, Frank Pfenning
Ordered type theory is an extension of linear type theory in which variables in the context may be neither dropped nor re-ordered. This restriction gives rise to a natural notion of adjacency. We...
A type theory for memory allocation and data layout (2003)
Leaf Petersen, Robert Harper, Karl Crary, Frank Pfenning
Ordered type theory is an extension of linear type theory in which variables in the context may be neither dropped nor re-ordered. This restriction gives rise to a natural notion of adjacency. We...
Umut A. Acar, Guy E. Blelloch, Robert Harper
We combine adaptivity and memoization to obtain an incremental computation technique that dramatically improves performance over adaptivity and memoization alone. The key contribution is adaptive...
A type system for higher-order modules (2003)
Derek Dreyer, Karl Crary, Robert Harper
We present a type theory for higher-order modules that accounts for many central issues in module system design, including translucency, applicativity, generativity, and modules as first-class...
A type theory for memory allocation and data layout (2003)
Leaf Petersen, Robert Harper, Karl Crary, Frank Pfenning
Abstract Ordered type theory is an extension of linear type theory in which variables in the context may be neither dropped nor re-ordered. This restriction gives rise to a natural notion of...
Corrigendum: Polymorphic Type Assignment and CPS Conversion (2003)
Robert Harper, Mark Lillibridge
It has come to our attention that there is an error in the proof of Theorem 6 on page 373 of the above titled paper [1]. Specifically, the term e ′ 0 does not type check in the system named DM as...
A type theory for memory allocation and data layout (2003)
Leaf Petersen, Robert Harper, Karl Crary, Frank Pfenning
Abstract Ordered type theory is an extension of linear type theory in which variables in the context may be neitherdropped nor re-ordered. This restriction gives rise to a natural notion of...
A Type Theory for Memory Allocation and Data Layout (2003)
Leaf Petersen Robert, Robert Harper, Karl Crary, Frank Pfenning
Ordered type theory is an extension of linear type theory in which variables in the context may be neither dropped nor re-ordered. This restriction gives rise to a natural notion of adjacency. We...
Umut A. Acar, Guy E. Blelloch, Robert Harper
We present a framework for applying memoization selectively. The framework provides programmer control over equality, space usage, and identification of precise dependences so that memoization can be...
Umut A. Acar, Guy E. Blelloch, Robert Harper
Although memoization is a powerful technique and can dramatically improve performance, it is often difficult to apply effectively. This is because significant performance improvements require the...
Umut Acar Guy, Guy E. Blelloch, Robert Harper
We present a framework for applying memoization selectively. The framework provides programmer control over equality, space usage, and identification of precise dependences so that memoization can be...
A Type System for Well-Founded Recursion (2003)
Derek Dreyer, Robert Harper, Karl Crary
In the interest of designing a recursive module extension to ML that is as simple and general as possible, we propose a novel type system for general recursion over eectful expressions. The presence...
Umut A. Acar, Guy E. Blelloch, Robert Harper
We combine adaptivity and memoization to obtain an incremental computation technique that dramatically improves performance over adaptivity and memoization alone. The key contribution is adaptive...
Development of an Optical Disc Recorder. (2002)
Kennedy,George, Zernike,F., Lou,D., Harper,Robert, Giebler,M.
Several air sandwich discs were fabricated and recordings made with them. Tellurium was chosen as the best material of those considered. Studies show that tellurium films are twice as sensitive as...
Adaptive functional programming (2002)
Umut A. Acar, Guy E. Blelloch, Robert Harper
An adaptive computation maintains the relationship between its input and output as the input changes. Although various techniques for adaptive computing have been proposed, they remain limited in...
Adaptive functional programming (2002)
Umut A. Acar, Guy E. Blelloch, Robert Harper
An adaptive computation maintains the relationship between its input and output as the input changes. Although various techniques for adaptive computing have been proposed, they remain limited in...
Adaptive functional programming (2002)
Umut A. Acar, Guy E. Blelloch, Robert Harper
An adaptive computation maintains the relationship between its input and output as the input changes. Although various techniques for adaptive computing have been proposed, they remained limited in...
Programming languages: Theory and practice (2002)
for his advice and suggestions, and to our students at both Carnegie Mellon and Princeton whose enthusiasm (and patience!) was instrumental in helping to create the course and this text. What follows...
Programming languages: Theory and practice (2002)
for his advice and suggestions, and to our students at both Carnegie Mellon and Princeton whose enthusiasm (and patience!) was instrumental in helping to create the course and this text. What follows...
Programming languages: Theory and practice (2002)
for his advice and suggestions, and to our students at both Carnegie Mellon and Princeton whose enthusiasm (and patience!) was instrumental in helping to create the course and this text. What follows...
A type system for higher-order modules (expanded version (2002)
Derek Dreyer, Karl Crary, Robert Harper
We present a type theory for higher-order modules that accounts for many central issues in module system design, including translucency, applicativity, generativity, and modules as first-class...
Derek Dreyer, Karl Crary, Robert Harper
Abstract We present a type theory for higher-order modules that accounts for many central issues in module system design, including translucency, applicativity, generativity, and modules as...
A type system for higher-order modules (expanded version (2002)
Derek Dreyer, Karl Crary, Robert Harper
We present a type theory for higher-order modules that accounts for many central issues in module system design, including translucency, applicativity, generativity, and modules as first-class...
Programming languages: Theory and practice (2002)
for his advice and suggestions, and to our students at both Carnegie Mellon and Princeton whose enthusiasm (and patience!) was instrumental in helping to create the course and this text. What follows...
A type system for higher-order modules (expanded version (2002)
Derek Dreyer, Karl Crary, Robert Harper
We present a type theory for higher-order modules that accounts for most current issues in modular programming languages, including translucency, applicativity, generativity, and modules as...
Trustless grid computing in ConCert (2002)
Karl Crary, Margaret Delap, Robert Harper, Jason Liszka, Tom Murphy Vii, ...
Abstract. We believe that fundamental to the establishment of a grid computing framework where all (not just large organizations) are able to e#ectively tap into the resources available on the global...
Trustless grid computing in ConCert (2002)
Karl Crary, Margaret Delap, Robert Harper, Jason Liszka, Tom Murphy Vii, ...
Abstract. We believe that fundamental to the establishment of a grid computing framework where all (not just large organizations) are able to eectively tap into the resources available on the global...
Trustless grid computing in ConCert (2002)
Karl Crary, Margaret Delap, Robert Harper, Jason Liszka, Tom Murphy Vii, ...
Abstract. We believe that fundamental to the establishment of a grid computing framework where all (not just large organizations) are able to e#ectively tap into the resources available on the global...
Adaptive functional programming (2002)
Umut A. Acar, Guy E. Blelloch, Robert Harper
An adaptive computation maintains the relationship between its input and output as the input changes. Although various techniques for adaptive computing have been proposed, they remained limited in...
Adaptive functional programming (2002)
Umut A. Acar, Guy E. Blelloch, Robert Harper
An adaptive computation maintains the relationship between its input and output as the input changes. Although various techniques for adaptive computing have been proposed, they remain limited in...
Adaptive functional programming (2002)
Umut A. Acar, Guy E. Blelloch, Robert Harper
An adaptive computation adapts its output to match changes to the input. Many techniques have been proposed for certain classes of adaptive computations, especially for particular applications such...
With the vast amount of computing resources distributed throughout the world today, the prospect of e#ectively harnessing these resources has captivated the imaginations of many and motivated both...
Towards a Functional Library for Fault-Tolerant (2002)
Margaret Delap, Jason Liszka, Tom Murphy Vii, Karl Crary, ...
To make development of grid applications less arduous, a natural, powerful, and convenient programming interface is required.
Trustless Grid Computing in ConCert (2002)
Karl Crary, Margaret Delap, Robert Harper, Jason Liszka, Tom Murphy Vii, ...
We believe that fundamental to the establishment of a grid computing framework where all (not just large organizations) are able to e#ectively tap into the resources available on the global network...
Derek Dreyer, Karl Crary, Robert Harper
Abstract We present a type theory for higher-order modules that accounts for many central issues in module systemdesign, including translucency, applicativity, generativity, and modules as...
Trustless grid computing in ConCert (2002)
Karl Crary, Margaret Delap, Robert Harper, Jason Liszka, Tom Murphy Vii, ...
Abstract. We believe that fundamental to the establishment of a grid computing framework where all (not just large organizations) are able to effectively tap into the resources available on the...
A type system for higher-order modules (expanded version (2002)
Derek Dreyer, Karl Crary, Robert Harper
We present a type theory for higher-order modules that accounts for many central issues in module system design, including translucency, applicativity, generativity, and modules as first-class...
Trustless grid computing in ConCert (2002)
Karl Crary, Margaret Delap, Robert Harper, Jason Liszka, Tom Murphy Vii, ...
Abstract. We believe that fundamental to the establishment of a grid computing framework where all (not just large organizations) are able to effectively tap into the resources available on the...
Adaptive functional programming (2002)
Umut A. Acar, Guy E. Blelloch, Robert Harper
An adaptive computation maintains the relationship between its input and output as the input changes. Although various techniques for adaptive computing have been proposed, they remain limited in...
With the vast amount of computing resources distributed throughout the world today, the prospect of effectively harnessing these resources has captivated the imaginations of many and motivated both...
Trustless grid computing in ConCert (2002)
Karl Crary, Margaret Delap, Robert Harper, Jason Liszka, Tom Murphy Vii, ...
Abstract. We believe that fundamental to the establishment of a grid computing framework where all (not just large organizations) are able to effectively tap into the resources available on the...
Adaptive functional programming (2002)
Umut A. Acar, Guy E. Blelloch, Robert Harper
An adaptive computation maintains the relationship between its input and output as the input changes. Although various techniques for adaptive computing have been proposed, they remain limited in...
An Effective Theory of Type Refinements (2002)
Yitzhak Mandelbaum, David Walker, Robert Harper
We develop an explicit two-level system that allows programmers to reason about the behavior of effectful programs. The first level is an ordinary ML-style type system, which confers standard...
A type system for higher-order modules (expanded version (2002)
Derek Dreyer, Karl Crary, Robert Harper
We present a type theory for higher-order modules that accounts for many current issues in modular programming languages, including translucency, applicativity, generativity, and modules as...
Trustless grid computing in ConCert (2002)
Karl Crary, Margaret Delap, Robert Harper, Jason Liszka, Tom Murphy Vii, ...
Abstract. We believe that fundamental to the establishment of a grid computing framework where all (not just large organizations) are able to effectively tap into the resources available on the...
Adaptive Functional Programming \Lambda (2002)
Umut A. Acar, Guy E. Blelloch, Robert Harper
Abstract An adaptive computation maintains the relationship between its input and output as the input changes. Although various techniques for adaptive computing have been proposed, they remain...
On Equivalence and Canonical Forms in the LF Type Theory (2001)
Harper, Robert, Pfenning, Frank
Decidability of definitional equality and conversion of terms into canonical form play a central role in the meta-theory of a type-theoretic logical framework. Most studies of definitional equality...
A Dependently Typed Assembly Language (2001)
We present a dependently typed assembly language (DTAL) in which the type system supports the use of a restricted form of dependent types, reaping some benefits of dependent types at assembly level....
A Dependently Typed Assembly Language (2001)
We present a dependently typed assembly language (DTAL) in which the type system supports the use of a restricted form of dependent types, reaping some benefits of dependent types at assembly level....
Toward a practical type theory for recursive modules (2001)
Derek R. Dreyer, Robert Harper, Karl Crary
Module systems for languages with complex type systems, such as Standard ML, often lack the ability to express mutually recursive type and function dependencies across module boundaries. Previous...
Toward a practical type theory for recursive modules (2001)
Derek R. Dreyer, Robert Harper, Karl Crary
Module systems for languages with complex type systems, such as Standard ML, often lack the ability to express mutually recursive type and function dependencies across module boundaries. Previous...
Automatic generation of staged geometric predicates (2001)
Aleksandar Nanevski, Guy Blelloch, Robert Harper
views and conclusions contained in this document are those of the authors and should not be interpreted as
A Dependently Typed Assembly Language (2001)
We present a dependently typed assembly language (DTAL) in which the type system supports the use of a restricted form of dependent types, reaping some benets of dependent types at the assembly...
A Dependently Typed Assembly Language (2001)
We present a dependently typed assembly language (DTAL) in which the type system supports the use of a restricted form of dependent types, reaping some benets of dependent types at the assembly...
Automatic generation of staged geometric predicates (2001)
Aleksandar Nanevski, Guy Blelloch, Robert Harper
Algorithms in Computational Geometry and Computer Aid-ed Design are often developed for the Real RAM model of computation, which assumes exactness of all the input arguments and operations. In...
Persistent triangulations (2001)
Guy Blelloch, Hal Burch, Karl Crary, Robert Harper, Gary Miller, Noel Walkington
Triangulations of a surface are of fundamental importance in computational geometry, computer graphics, and engineering and scientic simulations. Triangulations are ordinarily represented as mutable...
Persistent Triangulations (2001)
Guy Blelloch, Hal Burch, Karl Crary, Robert Harper, Gary Miller, Noel Walkington
this paper we will use the term fully persistent in the stronger sense that it must support parallelism.
Persistent Triangulations (2001)
Guy Blelloch Hal, Hal Burch, Karl Crary, Robert Harper, Gary Miller, Noel Walkington
Triangulations of a surface are of fundamental importance in computational geometry, engineering simulation, and computer graphics. For example, the convex hull of a set of points may be constructed...
Adaptive Functional Programming (2001)
Umut A. Acar, Guy E. Blelloch, Robert Harper
An adaptive computation maintains the relationship between its input and output as the input changes. Although various techniques for adaptive computing have been proposed, they remained limited in...
A Type System for Higher-Order Modules (2001)
Derek Dreyer, Karl Crary, Robert Harper
We present a type theory for higher-order modules that accounts for many current issues in modular programming languages, including translucency, applicativity, generativity, and modules as...
Modularity Matters Most (2001)
Karl Crary, Robert Harper, Peter Lee, Frank Pfenning
We contend that modularity is the key to improving software quality. We advocate a view of modularity that emphasizes not the mere assembling of software systems from component parts, but rather the...
Toward a practical type theory for recursive modules (2001)
Derek R. Dreyer, Robert Harper, Karl Crary
Module systems for languages with complex type systems, such as Standard ML, often lack the ability to express mutually recursive type and function dependencies across module boundaries. Previous...
Modularity Matters, Most Karl Crary, Robert Harper, Peter Lee, Frank Pfenning
Abstract We contend that modularity is the key to improving software quality. We advocate a view of modularity that emphasizes not the mere assembling of software systems from component parts, but...
Automated Techniques for Provably Safe Mobile Code (2001)
Christopher Colby, Karl Crary, Robert Harper, Peter Lee, Frank Pfenning
We present a general framework for provably safe mobile code. It relies on a formal definition of a safety policy and explicit evidence for compliance with this policy which is attached to a binary....
A Dependently Typed Assembly Language (2001)
We present a dependently typed assembly language (DTAL) in which the type system supports the use of a restricted form of dependent types, reaping some bene ts of dependent types at assembly level....
Automatic generation of staged geometric predicates (2001)
Aleksandar Nanevski, Guy Blelloch, Robert Harper
The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied, of the National Science...
Toward a practical type theory for recursive modules (2001)
Derek R. Dreyer, Robert Harper, Karl Crary
Abstract Module systems for languages with complex type systems, such as Standard ML, often lack the ability to express mutually recursive type and function dependencies across module boundaries....
Automatic generation of staged geometric predicates (2001)
Aleksandar Nanevski, Guy Blelloch, Robert Harper
views and conclusions contained in this document are those of the authors and should not be interpreted as
Persistent triangulations (2001)
Guy Blelloch, Hal Burch, Karl Crary, Robert Harper, Gary Miller, Noel Walkington
Triangulations of a surface are of fundamental importance in computational geometry, engineering simulation, and computer graphics. For example, the convex hull of a set of points may be constructed...
Adaptive Functional Programming (2001)
Umut Acar Guy, Guy E. Blelloch, Robert Harper
An adaptive computation maintains the relationship between its input and output as the input changes. Although various techniques for adaptive computing have been proposed, they remain limited in...
Automatic Generation of Staged Geometric Predicates (2001)
Aleksandar Nanevski, Guy Blelloch, Robert Harper
Algorithms in Computational Geometry and Computer Aid-ed Design are often developed for the Real RAM model of computation, which assumes exactness of all the input arguments and operations. In...
Modularity Matters Most (2001)
Karl Crary, Robert Harper, Peter Lee Z
Frank Pfenning x We contend that modularity is the key to improving software quality. We advocate a view of modularity that emphasizes not the mere assembling of software systems from component...
A Language-Based Approach to Security (2000)
Schneider, Fred, Morrisett, Greg, Harper, Robert
Language-based security leverages program analysis and program rewriting to enforce security policies. The approach promises efficient enforcement of fine-grained access control policies and depends...
A Language-Based Approach to Security (2000)
Schneider, Fred, Morrisett, Greg, Harper, Robert
Language-based security leverages program analysis and program rewriting to enforce security policies. The approach promises efficient enforcement of fine-grained access control policies and depends...
A language-based approach to security (2000)
Fred B. Schneider, Greg Morrisett, Robert Harper
Abstract. Language-based security leverages program analysis and program rewriting to enforce security policies. The approach promises efficient enforcement of fine-grained access control policies...
Implementing the TILT internal language (2000)
Leaf Petersen, Perry Cheng, Robert Harper, Chris Stone
The TILT compiler for Standard ML represents programs internally using a predicative lambda calculus based on Girard’s Fω. At the kind level, this language is notable for containing singleton...
Deciding type equivalence in a language with singleton kinds (2000)
Christopher A. Stone, Robert Harper
rwh+&s.cmu.edu
Automated Techniques for Provably Safe Mobile Code (2000)
Karl Crary, Robert Harper, Peter Lee, Frank Pfenning
We present a general framework for provably safe mobile code. It relies on a formal definition of a safety policy and explicit evidence for compliance with this policy that is attached to a binary....
Automated Techniques for Provably Safe Mobile Code (2000)
Karl Crary, Robert Harper, Peter Lee, Frank Pfenning
We present a general framework for provably safe mobile code. It relies on a formal definition of a safety policy and explicit evidence for compliance with this policy which is attached to a binary....
Deciding type equivalence in a language with singleton kinds (2000)
Christopher A. Stone, Robert Harper
Work on the TILT compiler for Standard ML led us to study a language with singleton kinds: S(A) is the kind of all types provably equivalent to the type A. Singletons are interesting because they...
Implementing the TILT internal language (2000)
Leaf Petersen, Perry Cheng, Robert Harper, Chris Stone
The TILT compiler for Standard ML represents programs internally using a predicative lambda calculus based on Girard's F. At the kind level, this language is notable for containing singleton...
On equivalence and canonical forms in the LF type theory (2000)
Decidability of definitional equality and conversion of terms into canonical form play a central role in the meta-theory of a type-theoretic logical framework. Most studies of definitional equality...
Implementing the TILT internal language (2000)
Leaf Petersen, Perry Cheng, Robert Harper, Chris Stone
The TILT compiler for Standard ML represents programs internally using a predicative lambda calculus based on Girard's F!. At the kind level, this language is notable for containing singleton...
A language-based approach to security (2000)
Fred B. Schneider, Greg Morrisett, Robert Harper
Abstract. Language-based security leverages program analysis and program rewriting to enforce security policies. The approach promises efficient enforcement of fine-grained access control policies...
Automated techniques for provably safe mobile code (2000)
Christopher Colby, Karl Crary, Robert Harper, Peter Lee, Frank Pfenning
We present a general framework for provably safe mobile code. It relies on a formal definition of a safety policy and explicit evidence for compliance with this policy which is attached to a binary....
Automated techniques for provably safe mobile code (2000)
Christopher Colby, Karl Crary, Robert Harper, Peter Lee, Frank Pfenning
We present a general framework for provably safe mobile code. It relies on a formal definition of a safety policy and explicit evidence for compliance with this policy which is attached to a binary....
On Equivalence and Canonical Forms (2000)
In The Lf, Robert Harper, Frank Pfenning
this paper we present a new, type-directed equivalence algorithm for the LF type theory that overcomes the weaknesses of previous approaches. The algorithm is practical, scales to richer languages,...
Automated Techniques for Provably Safe Mobile Code (2000)
Christopher Colby, Karl Crary, Robert Harper, Peter Lee, Frank Pfenning
We present a general framework for provably safe mobile code. It relies on a formal definition of a safety policy and explicit evidence for compliance with this policy which is attached to a binary....
Deciding type equivalence in a language with singleton kinds (2000)
Christopher A. Stone, Robert Harper
Abstract Work on the TILT compiler for Standard ML led us to study a language with singleton kinds: S(A) is the kind of all types provably equivalent to the type A. Singletons are interesting because...
On equivalence and canonical forms in the LF type theory (2000)
Decidability of de nitional equality and conversion of terms into canonical form play a central role in the meta-theory of a type-theoretic logical framework. Most studies of de nitional equality are...
On equivalence and canonical forms in the LF type theory (2000)
Decidability of definitional equality and conversion of terms into canonical form play a central role in the meta-theory of a type-theoretic logical framework. Most studies of definitional equality...
On equivalence and canonical forms in the LF type theory (2000)
Decidability of definitional equality and conversion of terms into canonical form play a central role in the meta-theory of a type-theoretic logical framework. Most studies of definitional equality...
Automated Techniques for Provably Safe Mobile Code (2000)
Karl Crary, Robert Harper, Peter Lee, Frank Pfenning
We present a general framework for provably safe mobile code. It relies on a formal definition of a safety policy and explicit evidence for compliance with this policy which is attached to a binary....
A language-based approach to security (2000)
Fred B. Schneider, Greg Morrisett, Robert Harper
Abstract. Language-based security leverages program analysis and program rewriting to enforce security policies. The approach promises efficient enforcement of fine-grained access control policies...
A Language-Based Approach to Security (2000)
Fred Schneider Greg, Fred B. Schneider, Greg Morrisett, Robert Harper
Language-based security leverages program analysis and program rewriting to enforce security policies. The approach promises e#- cient enforcement of fine-grained access control policies and depends...
Implementing the TILT internal language (2000)
Leaf Petersen, Perry Cheng, Robert Harper, Chris Stone
The TILT compiler for Standard ML represents programs internally using a predicative lambda calculus based on Girard's F!. At the kind level, this language is notable for containing singleton...
On Equivalence and Canonical Forms intheLFTypeTheory (2000)
Decidability of definitional equality and conversion of terms into canonical form play a central role in the meta-theory of a type-theoretic logical framework. Most studies of definitional equality...
A language-based approach to security (2000)
Fred B. Schneider, Greg Morrisett, Robert Harper
Abstract. Language-based security leverages program analysis and program rewriting to enforce security policies. The approach promises efficient enforcement of fine-grained access control policies...
On Equivalence and Canonical Forms intheLFTypeTheory (2000)
Decidability of definitional equality and conversion of terms into canonical form play a central role in the meta-theory of a type-theoretic logical framework. Most studies of definitional equality...
Deciding type equivalence in a language with singleton kinds (2000)
Christopher A. Stone, Robert Harper
Work on the TILT compiler for Standard ML led us to study a language with singleton kinds: S(A) is the kind of all types provably equivalent to the type A. Singletons are interesting because they...
On Equivalence and Canonical Forms (2000)
In The Lf, Robert Harper, Frank Pfenning
this paper we present a new, type-directed equivalence algorithm for the LF type theory that overcomes the weaknesses of previous approaches. The algorithm is practical, scales to richer languages,...
Research Intern. Advised by Simon Peyton-Jones. I designed and implemented a new feature called view patterns for GHC, a compiler for the programming language Haskell. Publications:
Thesis (M.A.)--University of California, Santa Barbara, 1999.
What is a recursive module (1999)
Karl Crary, Robert Harper, Sidd Puri
A hierarchical module system is an effective tool for structuring large programs. Strictly hierarchical module systems impose an acyclic ordering on import dependencies among program units. This can...
What is a Recursive Module? (1999)
Karl Crary, Robert Harper, Sidd Puri
A hierarchical module system is an effective tool for structuring large programs. Strictly hierarchical module systems impose an acyclic ordering on import dependencies among program units. This can...
Persistent Triangulations (1999)
Guy Blelloch Hal, Hal Burch, Karl Crary, Robert Harper, Gary Miller, Noel Walkington
Triangulations of a surface are of fundamental importance in computational geometry, engineering simulation, and computer graphics. For example, the convex hull of a set of points may be constructed...
Parametricity and variants of Girard's J operator (1999)
Robert Harper, John C. Mitchell
The Girard-Reynolds polymorphic -calculus is generally regarded as a calculus of parametric polymorphism in which all well-formed terms are strongly normalizing with respect to fi-reductions. Girard...
On Equivalence and Canonical Forms in the LF Type Theory (1999)
Decidability of definitional equality and conversion of terms into canonical form play a central role in the meta-theory of a type-theoretic logical framework. Most studies of definitional equality...
A Dependently Typed Assembly Language (1999)
We present a dependently typed assembly language (DTAL) in which the type system supports the use of a restricted form of dependent types, reaping some benets of dependent types at assembly level....
Deciding Type Equivalence in a Language with Singleton Kinds (1999)
Christopher A. Stone, Robert Harper
Work on the TILT compiler for Standard ML led us to study a language with singleton kinds: S(A) is the kind of all types provably equivalent to the type A. Singletons are interesting because they...
Deciding Type Equivalence in a Language with Singleton Kinds (1999)
Christopher A. Stone, Robert Harper
Work on the TILT compiler for Standard ML led us to study a language with singleton kinds: S(A) is the kind of all types provably equivalent to the type A. Singletons are interesting because they...
A Dependently Typed Assembly Language (Extended Abstract) (1999)
We present a dependently typed assembly language (DTAL) in which the type system supports the use of a restricted form of dependent types, reaping some bene ts of dependent types at assembly level....
On Equivalence and Canonical Forms in the LF Type Theory (1999)
Decidability of definitional equality and conversion of terms into canonical form play a central role in the meta-theory of a type-theoretic logical framework. Most studies of definitional equality...
On Equivalence and Canonical Forms in the LF Type Theory (Extended Abstract) (1999)
Decidability of definitional equality and conversion of terms into canonical form play a central role in the meta-theory of a type-theoretic logical framework. Most studies of definitional equality...
Persistent Triangulations (1999)
Guy Blelloch, Hal Burch, Karl Crary, Robert Harper, Gary Millor, Noel Walkington
Triangulations of a surface are of fundamental importance in computational geometry, engineering simulation, and computer graphics. For example, the convex hull of a set of points may be constructed...
A Dependently Typed Assembly Language (Extended Abstract) (1999)
) Hongwei Xi Oregon Graduate Institute hongwei@cse.ogi.edu Robert Harper Carnegie Mellon University rwh@cs.cmu.edu Abstract We present a dependently typed assembly language (DTAL) in which the type...
What is a Recursive Module? (1999)
Karl Crary, Robert Harper, Sidd Puri
A hierarchical module system is an effective tool for structuring large programs. Strictly hierarchical module systems impose an acyclic ordering on import dependencies among program units. This can...
Deciding Type Equivalence in a Language with Singleton Kinds (1999)
Christopher Stone, Robert Harper
Work on the TILT compiler for Standard ML led us to study a language with singleton kinds: S(A) is the kind of all types provably equivalent to the type A. Singletons are interesting because they...
What is a Recursive Module? (1999)
Karl Crary, Robert Harper, Sidd Puri
A hierarchical module system is an effective tool for structuring large programs. Strictly hierarchical module systems impose an acyclic ordering on import dependencies among program units. This can...
On Equivalence and Canonical Forms intheLFTypeTheory (1999)
Decidability of definitional equality and conversion of terms into canonical form play a central role in the meta-theory of a type-theoretic logical framework. Most studies of definitional equality...
On Equivalence and Canonical Forms in the LF Type Theory (Extended Abstract) ∗ (1999)
Decidability of definitional equality and conversion of terms into canonical form play a central role in the meta-theory of a type-theoretic logical framework. Most studies of definitional equality...
Christopher A. Stone, Singleton Kinds, Robert Harper
Work on the TILT compiler for Standard ML led us to study a language with singleton kinds: S(A) is the kind of all types provably equivalent tothetype A. Singletons are interesting because they...
On Equivalence and Canonical Forms in the LF Type Theory (Extended Abstract) (1999)
Decidability of de nitional equality and conversion of terms into canonical form play a central role in the meta-theory of a type-theoretic logical framework. Most studies of de nitional equality are...
What is a recursive module (1999)
Karl Crary, Robert Harper, Sidd Puri
A hierarchical module system is an e ective tool for structuring large programs. Strictly hierarchical module systems impose an acyclic ordering on import dependencies among program units. This can...
Typing First-Class Continuations in ML, (1998)
Duba, Bruce F., Harper, Robert, MacQueen, David
First-class continuations are a powerful tool for implementing sophisticated control constructs like co-routines, processes, backtracking, and asynchronous signals. Until now they have been studied...
Polymorphic Type Assignment and CPS Conversion, (1998)
Harper, Robert, Lillibridge, Mark
Meyer and Wand established that the type of a term in the simply typed lambda-calculus may be related in a straightforward manner to the type of its call-by-value CPS transform. This typing property...
A Module System for a Programming Language Based on the LF Logical Framework. (1998)
Harper, Robert, Pfenning, Frank
We describe a module system for Elf, a logic programming language based on the LF logical framework. The static part of module calculus addresses name-space management and structured presentation of...
Explicit Polymorphism and CPS Conversion, (1998)
Harper, Robert, Lillibridge, Mark
We study the typing properties of CPS conversion for an extension of F omega, with control operators. Two classes of evaluation strategies are considered, each with call-by-name and call-by-value...
Note on Conditional Compilation in Standard ML, (1998)
Haines, Nicholas, Biagioni, Edoardo, Milnes, Brian G., Harper, Robert
In the Fox project we make frequent use of conditional code within Standard ML functors: code which depends on the functor arguments. The canonical example is instrumentation code for testing or...
A Simplified Account of Polymorphic References. Revised. (1998)
The extension of Damas and Milner's polymorphic type system for pure functional programs (2) to accommodate mutable cells has proved to be problematic. The naive extension of the pure language with...
Standard ML Signatures for a Protocol Stack, (1998)
Biagioni, Edoardo, Harper, Robert, Lee, Peter
This paper describes the design of a protocol stack implemented in Standard ML. Standard ML's signatures are a language construct which can be used to specify or constrain the interface of a module....
Incremental Recompilation for Standard ML of New Jersey. (1998)
Harper, Robert, Pfenning, Frank, Lee, Peter, Rollins, Eugene
Probabilistic planning methods can have various objectives: usually they either maximize the probability of goal achievement or minimize the expected execution cost of the plan, and therefore assume...
Compiling with Non-Parametric Polymorphism. (1998)
Harper, Robert, Morrisett, Greg
There is a middle ground between parametric and ad-hoc polymorphism in which a computation can depend upon a type parameter but is restricted to being defined at all types in an inductive fashion. We...
Abstract Models of Memory Management. (1998)
Morrisett, Greg, Felleisen, Mattias, Harper, Robert
Most specifications of garbage collectors concentrate on the low-level algorithmic details of how to find and preserve accessible objects. Often, they focus on bit-level manipulations such as...
An Interpretation of Standard ML in Type Theory (1998)
Harper, Robert, Stone, Christopher
We define an interpretation of Standard ML into type theory. The interpretation takes the form of a set of elaboration rules reminiscent of the static semantics given in The Definition of Standard...
The Fox Project: Advanced Language Technology for Extensible Systems (1998)
Harper, Robert, Lee, Peter, Pfenning, Frank
It has been amply demonstrated in recent years that careful attention to the structure of systems software can lead to greater flexibility, reliability, and ease of implementation, without incurring...
Relational Interpretations of Recursive Types in an Operational Setting (1998)
Birkedal, Lars, Harper, Robert
Relational interpretations of type systems are useful for establishing properties of programming languages. For languages with recursive types it is usually difficult to establish the existence of a...
Eversmeyer, Kent E., Henley, Jess, Harper, Robert, Talbert, Dan, Caruso, Gerald
This paper provides an overview of the innovative solutions developed to meet the requirements of the target set designed for the Ground Based Radar Prototype (GBR-P) Radar Credible Target (RCT-1)...
What is a Recursive Module? (1998)
Crary, Karl, Harper, Robert, Puri, Sidd
Hierarchical decomposition is a fundamental design principle for controlling the complexity of large programs. According to this principle a software system is to be decomposed into a collection of...
Transparent and Opaque Interpretations of Datatypes (1998)
Crary, Karl, Harper, Robert, Cheng, Perry, Petersen, Leaf, Stone, Chris
Standard ML employs an opaque (or generative) interpretation of datatype specifications, in which every datatype specification provides a new, abstract type that is different from any other type,...
Deciding Type Equivalence in a Language with Singleton Kinds, (1998)
Stone, Christopher A., Harper, Robert
Work on the TILT compiler for Standard ML led us to study a language with singleton kinds: S(A) is the kind of all types provably equivalent to the type A. Singletons are interesting because they...
On Equivalence and Canonical Forms in the LF Type Theory (1998)
Harper, Robert, Pfenning, Frank
Decidability of definitional equality and conversion of terms into canonical form play a central role in the meta-theory of a type-theoretic logical framework. Most studies of definitional equality...
A Language-Based Approach to Security (1998)
Schneider, Fred B., Morrisett, Greg, Harper, Robert
Language based security leverages program analysis and program rewriting to enforce security policies. The approach promises efficient enforcement of fine grained access control policies and depends...
Implementing the TILT Internal Language (1998)
Petersen, Leaf, Cheng, Perry, Harper, Robert, Stone, Chris
The TILT compiler for Standard ML represents programs internally using a predicative lambda calculus based on Girard's F omega. At the kind level, this language is notable for containing singleton...
Eversmeyer, Kent E., Harper, Robert, Talbert, Dan, Caruso, Gerald, Tucker, Robert
This paper provides an overview of the targets planned for the SBIRS-Low Dedicated Target missions, SDT-1 and SDT-2. Results from the process of developing a common set of targets to meet the dual...
Typed Closure Conversion for Recursively-Defined Functions (Extended Abstract) (1998)
Closure conversion is a critical program transformation for higher-order languages that eliminates lexically nested, first-class functions or procedures. In particular, closure conversion translates...
A Type-Theoretic Interpretation of Standard ML (1998)
Robert Harper, Christopher Stone
ion boundaries must be broken at run-time. Consequently, an association between the abstract stamps and their underlying representations must be maintained. In this paper we outline an interpretation...
Transparent and Opaque Interpretations of Datatypes (1998)
Karl Crary, Robert Harper, Perry Cheng, Leaf Petersen, Chris Stone, Signature Sig
type along with introduction and elimination functions for that type [2]: signature SIG1 opaque = sig type u type t = u * u val u in : (u * u + int) -? u val u out : u -? (u * u + int) end signature...
Relational Interpretations of Recursive Types in an Operational Setting (1998)
Relational interpretations of type systems are useful for establishing properties of programming languages. For languages with recursive types it is usually difficult to establish the existence of a...
Generational Stack Collection and Profile-Driven Pretenuring (1998)
Perry Cheng, Robert Harper, Peter Lee
This paper presents two techniques for improving garbage collection performance: generational stack collection and profile-driven pretenuring. The first is applicable to stackbased implementations of...
The Fox Project: Advanced Language Technology for Extensible Systems (1998)
Robert Harper, Peter Lee, Frank Pfenning
It has been amply demonstrated in recent years that careful attention to the structure of systems software can lead to greater flexibility, reliability, and ease of implementation, without incurring...
How Generic is a Generic Back End? Using MLRISC as a Back End for the TIL Compiler (1998)
Andrew Bernard, Robert Harper, Peter Lee
. We describe the integration of MLRISC, a "generic" compiler back end, with TIL, a type-directed compiler for Standard ML. The TIL run-time system uses a form of type information to enable...
Typed closure conversion for recursively-defined functions (extended abstract (1998)
) Greg Morrisett 1 Cornell University Robert Harper 2 Carnegie Mellon University Abstract Much recent work on the compilation of statically typed languages such as ML relies on the propagation of...
A Type-Theoretic Interpretation of Standard ML (1998)
this document are those of the authors and should not be interpreted as representing official policies, either expressed or implied, of the Advanced Research Projects Agency, the U.S. Government or...
A Type-Theoretic Interpretation of Standard ML (1998)
this document are those of the authors and should not be interpreted as representing official policies, either expressed or implied, of the Advanced Research Projects Agency, the U.S. Government or...
Transparent and Opaque Interpretations of Datatypes (1998)
Karl Crary, Robert Harper, Perry Cheng, Leaf Petersen, Chris Stone
this document are those of the authors and should not be interpreted as representing official policies, either expressed or implied, of the Defense Advanced Research Projects Agency or the U.S....
The Fox project: Advanced language technology for extensible systems (1998)
Robert Harper, Peter Lee, Frank Pfenning
should not be interpreted as representing official policies, either expressed or implied, of
Karl Crary, Robert Harper, Perry Cheng, Leaf Petersen, Chris Stone
Standard ML employs an opaque (or generative) interpretation of datatype type that is di erent from any other type, including other identically speci ed datatypes. An alternative interpretation is...
Transparent and opaque interpretations of datatypes (1998)
Karl Crary, Robert Harper, Perry Cheng, Leaf Petersen, Chris Stone
views and conclusions contained in this document are those of the authors and should not be interpreted as representing o cial policies, either expressed or implied, of the Defense Advanced Research...
Recursive Types in an Operational Setting (1998)
Lars Birkedal, Robert Harper, Lars Birkedal
A summary of some of the results in this paper appeared in TACS '97.
Generational stack collection and profile-driven pretenuring (1998)
Perry Cheng, Robert Harper, Peter Lee
This paper presents two techniques for improving garbage collection performance: generational stack collection and profile-driven pretenuring. The first is applicable to stack-based implementations...
A Module System for a Programming Language Based on the LF Logical Framework (1998)
HARPER, ROBERT, PFENNING, FRANK
We describe a module system for Elf, a logic programming language based on the LF logical framework. The static part of the module calculus addresses name-space management and structured presentation...
TIL: A Type-Directed Optimizing Compiler for ML. (1997)
Tarditi, David, Stone, Chris, Morrisett, Greg, Harper, Robert, Cheng, Perry
We describe a new compiler for Standard ML called TIL, that is based on four technologies: intensional polymorphism, tag-free garbage collection, conventional functional language optimization and...
A Type-Theoretic Account of Standard ML 1996 (Version 1). (1997)
A type-theoretic definition of a variant of the Standard ML (Revised 1996) programming language is given. The definition consists of a syntax-directed translation of SML96 programs into a typed...
An interpretation of Standard ML in type theory (1997)
Robert Harper, Christopher Stone
elaboration, static semantics, dynamic semantics We de ne an interpretation of Standard ML into type theory. The interpretation takes the form of a set of elaboration rules reminiscent of the static...
Relational interpretations of recursive types in an operational setting (1997)
Abstract. Relational interpretations of type systems are a useful tool for establishing properties of programming languages. For languages with recursive types the existence of a relational...
Types in Programming Language Design and Implementation (1997)
s. The informal notion of safety emerges as "progress" and "preservation" properties relating the operational semantics to the type system. Enforcement of data abstraction...
Semantics of Memory Management for Polymorphic Languages (1997)
We present a static and dynamic semantics for an abstract machine that evaluates expressions of a polymorphic programming language. Unlike traditional semantics, our abstract machine exposes many...
Relational Interpretations of Recursive Types in an Operational Setting (1997)
Robert Harper, Lars Birkedal, Lars Birkedal
Relational interpretations of type systems are useful for establishing properties of programming languages. For languages with recursive types it is difficult to establish the existence of a...
Semantics of Memory Management for Polymorphic Languages (1997)
We present a static and dynamic semantics for an abstract machine that evaluates expressions of a polymorphic programming language. Unlike traditional semantics, our abstract machine exposes many...
George C. Necula, Robert Harper, Frank Pfenning
I propose a new compiler architecture for compiling source-level programs into a combination of object code and a proof that the object code preserves certain properties of the source program. Such a...
Semantics of memory management for polymorphic languages (1997)
We present a static and dynamic semantics for an abstract machine that evaluates expressions of a polymorphic programming language. Unlike traditional semantics, our abstract machine exposes many...
Relational interpretations of recursive types in an operational setting (1997)
Abstract. Relational interpretations of type systems are a useful tool for establishing properties of programming languages. For languages with recursive types the existence of a relational...
Semantics of memory management for polymorphic languages (1997)
The views and conclusions contained in this document arethose of the authors and should not be interpreted as representing o cial policies, either expressed or implied, of the Advanced We present a...
Relational interpretations of recursive types in an operational setting (1997)
Submitted for publication to Information and Computation. A summary of this paper appeared in TACS '97.
Operational Interpretations of an Extension of Fω with Control Operators (1996)
Robert Harper, Mark Lillibridge
We study the operational semantics of an extension of Girard’s System Fω with two control operators: an abort operation that abandons the current control context, and a callcc operation that...
TIL: A type-directed optimizing compiler for ML (1996)
David Tarditi, Greg Morrisett, Perry Cheng, Chris Stone, Robert Harper, Peter Lee
We describe a new compiler for Standard ML called TIL, that is based on four technologies: intensional polymorphism, tag-free garbage collection, conventional functional language optimization, and...
The TIL/ML Compiler: Performance and Safety through Types (1996)
Greg Morrisett, David Tarditi, Perry Cheng, Chris Stone, P. Cheng, Peter Lee, ...
Systems code requires both high performance and reliability. Usually, these two goals are at odds with each other. For example, to prevent kernel data structures from being over-written or read,...
Typed Closure Conversion (1996)
Yasuhiko Minamide, Greg Morrisett, Robert Harper
We study the typing properties of closure conversion for simply-typed and polymorphic -calculi. Unlike most accounts of closure conversion, which only treat the untyped -calculus, we translate...
Typed Closure Conversion (1996)
Yasuhiko Minamide, Greg Morrisett, Robert Harper
We study the typing properties of closure conversion for simply-typed and polymorphic -calculi. Unlike most accounts of closure conversion, which only treat the untyped -calculus, we translate...
Type Systems for Programming Languages (1996)
Types 49 6.1 Statics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 6.2 Dynamics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 6.3 Impredicativity . . . . . ....
Typed Closure Conversion (1996)
Yasuhiko Minamide, Greg Morrisett, Robert Harper
Closure conversion is a program transformation used by compilers to separate code from data. Previous accounts of closure conversion use only untyped target languages. Recent studies show that...
Typed Closure Conversion (1996)
Yasuhiko Minamide, Greg Morrisett, Robert Harper
We study the typing properties of closure conversion for simply-typed and polymorphic -calculi. Unlike most accounts of closure conversion, which only treat the untyped -calculus, we translate...
Typed Closure Conversion (1996)
Yasuhiko Minamide, Greg Morrisett, Robert Harper
We study the typing properties of closure conversion for simply-typed and polymorphic -calculi. Unlike most accounts of closure conversion, which only treat the untyped -calculus, we translate...
Typed Closure Conversion (1996)
Yasuhiko Minamide, Greg Morrisett, Robert Harper
Closure conversion is a program transformation used by compilers to separate code from data. Previous accounts of closure conversion use only untyped target languages. Recent studies show that...
TIL: A Type-Directed Optimizing Compiler for ML (1996)
David Tarditi, Greg Morrisett, Perry Cheng, Chris Stone, Robert Harper, Peter Lee
We describe a new compiler for Standard ML called TIL, that is based on four technologies: intensional polymorphism, tag-free garbage collection, conventional functional language optimization, and...
A Type-Theoretic Account of Standard ML 1996 (Version 2) (1996)
A type-theoretic definition of a variant of the Standard ML (Revised 1996) programming language is given. The definition consists of a syntax-directed elaboration of SML '96 programs into a...
Typed closure conversion (1996)
Yasuhiko Minamide, Greg Morrisett, Robert Harper
The views and conclusions contained in this document are those of the authors and should not be interpreted as representing o cial policies, either expressed or implied, of the Advanced Research...
Compiling Polymorphism Using Intensional Type Analysis (1995)
Traditional techniques for implementing polymorphism use a universal representation for objects of unknown type. Often, this forces a compiler to use universal representations even if the types of...
TIL: A Type-Directed Optimizing Compiler for ML (1995)
David Tarditi, Greg Morrisett, Perry Cheng, Chris Stone, Robert Harper, Peter Lee
We describe a new compiler for Standard ML called TIL, that is based on four technologies: intensional polymorphism, tag-free garbage collection, conventional functional language optimization, and...
Compiling Polymorphism Using Intensional Type Analysis (1995)
Types have been used to describe the size and shape of data structures at compile time. In polymorphic languages or languages with abstract types, this is not possible since the types of some objects...
Compiling Polymorphism Using Intensional Type Analysis (1995)
Types have been used to describe the size and shape of data structures at compile time. In polymorphic languages or languages with abstract types, this is not possible since the types of some objects...
TIL: A Type-Directed, Optimizing Compiler for ML (1995)
David Tarditi, Greg Morrisett, Perry Cheng, Chris Stone, Robert Harper, Peter Lee
The goal of the TIL project was to explore the use of Typed Intermediate Languages to produce high-performance native code from Standard ML (SML). We believed that existing SML compilers were doing a...
Yasuhiko Minamide 1 Typed Closure Conversion (1995)
The views and conclusions contained in this document are those of the authors and should not be interpreted as representing o cial policies, either expressed or implied, of the Advanced Research...
Abstract models of memory management (1995)
Greg Morrisett, Matthias Felleisen, Robert Harper
U.S. Government.
Compiling polymorphism using intensional type analysis (1995)
The views and conclusions contained in this document are those of the authors and should not be interpreted as
Thesis (MD)--Queen's University of Belfast, 1994.
A type-theoretic approach to higher-order modules with sharing (1994)
Robert Harper, Mark Lillibridge
The design of a module system for constructing and maintaining large programs is a difficult task that raises a number of theoretical and practical issues. A fundamental issue is the management of...
A compilation manager for standard ML of New Jersey (1994)
Robert Harper, Frank Pfenning, Peter Lee, Eugene Rollins
The design and implementation of a compilation manager (CM) for Standard ML of New Jersey (SML/NJ) is described. Truly independent compilation is difficult to implement correctly and efficiently for...
Andrzej Tarlecki Draft, Robert Harper, Donald Sannella, Andrzej Tarlecki
The purpose of a logical framework such as LF is to provide a language for defining logical systems suitable for use in a logic-independent proof development environment. All inferential activity in...
A Type-Theoretic Approach to Higher-Order Modules with Sharing (1994)
Robert Harper, Mark Lillibridge
The design of a module system for constructing and maintaining large programs is a difficult task that raises a number of theoretical and practical issues. A fundamental issue is the management of...
Andrzej Tarlecki Draft, Robert Harper, Donald Sannella, Andrzej Tarlecki
The purpose of a logical framework such as LF is to provide a language for defining logical systems suitable for use in a logic-independent proof development environment. All inferential activity in...
Implementing Software Architectures in Standard ML (1994)
Edoardo Biagioni, Robert Harper, Peter Lee
ions Using Signatures The key to composability in a layered system architecture is to arrange for each layer to satisfy a standard interface. If every component satisfies the standard interface, and...
Advanced Languages for Systems Software The Fox Project in 1994 (1994)
It has been amply demonstrated in recent years that careful attention to the structure of systems software can lead to greater flexibility, reliability, and ease of implementation, without incurring...
Compiling with Non-Parametric Polymorphism (Preliminary Report) (1994)
Robert Harper And, Robert Harper, Greg Morrisett
There is a middle ground between parametric and ad-hoc polymorphism in which a computation can depend upon a type parameter but is restricted to being defined at all types in an inductive fashion. We...
Structured Theory Presentations and Logic Representations (1994)
Robert Harper, Donald Sannella, Andrzej Tarlecki
The purpose of a logical framework such as LF is to provide a language for defining logical systems suitable for use in a logic-independent proof development environment. All inferential activity in...
Advanced Languages for Systems Software The Fox Project in 1994 (1994)
Robert Harper And, Robert Harper, Peter Lee
It has been amply demonstrated in recent years that careful attention to the structure of systems software can lead to greater flexibility, reliability, and ease of implementation, without incurring...
Type Theory for Programming Languages (1994)
Types 83 9.1 Syntax : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 83 9.2 Typing Rules : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 83 9.3 Operational Semantics : : :...
Incremental Recompilation for Standard ML of New Jersey (1994)
Robert Harper, Frank Pfennig, Peter Lee, Eugene Rollins
The design and implementation of an incremental recompilation manager (IRM) for Standard ML of New Jersey (SML/NJ) is described. Truly separate compilation is difficult to implement correctly and...
A Simplified Account of Polymorphic References (1994)
A proof of the soundness of Tofte's imperative type discipline with respect to a structured operational semantics is given. The presentation is based on a semantic formalism that combines the...
A Simpli ed Account ofPolymorphic References (1994)
A proof of the soundness of Tofte's imperative type discipline with respect to a structured operational semantics is given. The presentation is based on a semantic formalism that combines the...
Atype-theoretic approach to higher-order modules with sharing (1994)
Robert Harper, Mark Lillibridge
The views and conclusions contained in this document are those of the authors and should not be interpreted as
A Framework for Defining Logics (1993)
Plotkin, Gordon, Honsell, Furio, Harper, Robert
The Edinburgh Logical Framework (LF) provides a means to define (or present) logics. It is based on a general treatment of syntax, rules, and proofs by means of a typed λ-calculus with dependent...
A Framework for Defining Logics (1993)
Plotkin, Gordon, Honsell, Furio, Harper, Robert
The Edinburgh Logical Framework (LF) provides a means to define (or present) logics. It is based on a general treatment of syntax, rules, and proofs by means of a typed -calculus with dependent...
Explicit polymorphism and CPS conversion (1993)
Robert Harper, Mark Lillibridge
We study the typing properties of CPS conversion for an extension of F! with control operators. Two classes of evaluation strategies are considered, each with call-by-name and call-by-value variants....
Standard ML Signatures for a Protocol Stack (1993)
Edoardo Biagioni, Robert Harper, Peter Lee
This paper describes the design of a protocol stack implemented in Standard ML. Standard ML's signatures are a language construct which can be used to specify or constrain the interface of a...
A framework for defining logics (1993)
Robert Harper, Furio Honsell, Gordon Plotkin
The Edinburgh Logical Framework (LF) provides a means to define (or present) logics. It is based on a general treatment of syntax, rules, and proofs by means of a typed-calculus with dependent types....
Note on Conditional Compilation in Standard ML (1993)
Nicholas Haines Edoardo, Nicholas Haines, Edoardo Biagioni, Robert Harper, Brian G. Milnes
In the Fox project we make frequent use of conditional code within Standard ML functors: code which depends on the functor arguments. The canonical example is instrumentation code for testing or...
Explicit Polymorphism and CPS Conversion (1993)
Robert Harper, Mark Lillibridge
We study the typing properties of CPS conversion for an extension of F ! with control operators. Two classes of evaluation strategies are considered, each with call-by-name and call-by-value...
A Type-Theoretic Approach to Higher-Order Modules with Sharing (1993)
Robert Harper, Mark Lillibridge
The design of a module system for constructing and maintaining large programs is a difficult task that raises a number of theoretical and practical issues. A fundamental issue is the management of...
A Simplified Account of Polymorphic References (1993)
A proof of the soundness of Tofte's imperative type discipline with respect to a structured operational semantics is given. The presentation is based on a semantic formalism that combines the...
A Simplified Account of Polymorphic References (1993)
A proof of the soundness of Tofte's imperative type discipline with respect to a structured operational semantics is given. The presentation is based on a semantic formalism that combines the...
Explicit Polymorphism and CPS Conversion (1993)
Robert Harper, Mark Lillibridge
We study the typing properties of CPS conversion for an extension of F! with control operators. Two classes of evaluation strategies are considered, each with call-by-name and call-by-value variants....
Standard ML Signatures for a Protocol Stack (1993)
Edoardo Biagioni, Robert Harper, Peter Lee
This paper describes the design of a protocol stack implemented in Standard ML. Standard ML's signatures are a language construct which can be used to specify or constrain the interface of a...
Functional Pearls: Proof-Directed Debugging (1993)
The close relationship between writing programs and proving theorems has frequently been cited as an advantage of functional programming languages. We illustrate the interplay between programming and...
Operational Interpretations of an Extension of F-omega with Control Operators (1993)
Robert Harper, Mark Lillibridge
We study the operational semantics of an extension of Girard's System F-omega with two control operators: an _abort_ operation that abandons the current control context, and a _callcc_ operation...
A framework for defining logics (1993)
Robert Harper, Furio Honsell, Gordon Plotkin
The Edinburgh Logical Framework (LF) provides a means to define (or present) logics. It is based on a general treatment of syntax, rules, and proofs by means of a typed λ-calculus with dependent...
Polymorphic type assignment and CPS conversion (1993)
Robert Harper, Mark Lillibridge
Meyer and Wand established that the type of a term in the simply typed-calculus may be related in a straightforward manner to the type of its call-by-value CPS transform. This typing property maybe...
Polymorphic type assignment and CPS conversion (1992)
Robert Harper, Mark Lillibridge
Meyer and Wand established that the type of a term in the simply typed λ-calculus may be related in a straightforward manner to the type of its call-by-value CPS transform. This typing property may...
Polymorphic type assignment and CPS conversion (1992)
Robert Harper, Mark Lillibridge
Abstract. Meyer and Wand established that the type of a term in the simply typed λcalculus may be related in a straightforward manner to the type of its call-by-value CPS transform. This typing...
On the Type Structure of Standard ML (1992)
Robert Harper, John C. Mitchell
Standard ML is a useful programming language with a polymorphic type system and a flexible module facility. One notable feature of the core expression language of ML is that it is implicitly typed:...
Polymorphic Type Assignment and CPS Conversion (1992)
Robert Harper, Mark Lillibridge
Meyer and Wand established that the type of a term in the simply typed lambda-calculus may be related in a straightforward manner to the type of its call-by-value CPS transform. This typing property...
Polymorphic Type Assignment and CPS Conversion (1992)
Robert Harper, Mark Lillibridge
Meyer and Wand established that the type of a term in the simply typed lambda-calculus may be related in a straightforward manner to the type of its call-by-value CPS transform. This typing property...
Electronic communications and the new biology (1992)
Bleasby, Alan, Griffiths, Paul, Harper, Robert, Hines, David, Hoover, Kenton, Kristofferson, David, ...
Typing first-class continuations in ML (1991)
Bruce F. Duba, Robert Harper, David Macqueen
An extension of Standard ML with continuation primitives similar to those found in Scheme is considered. A number of alternative type systems are discussed, and several programming examples are...
Type Checking with Universes (1991)
Various formulations of constructive type theories have been proposed to serve as the basis for machine-assisted proof and as a theoretical basis for studying programming languages. Many of these...
Typing First-Class Continuations in ML (1991)
Bruce F. Duba, Robert Harper, David Macqueen
An extension of Standard ML with continuation primitives similar to those found in Scheme is considered. A number of alternative type systems are discussed, and several programming examples are...
The Fox Project: Advanced Development of Systems Software (1991)
Eric Cooper, Robert Harper, Peter Lee
The Fox project will use an advanced programming language to build software such as operating systems, network protocols, and distributed systems. The goals of the project are to improve the design...
Modularity in the LF Logical Framework (1991)
this paper we make a concrete proposal for a module system for the Elf language which attempts to address those three central issues. Various approaches to the static and dynamic semantics of such a...
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...
Modularity in the LF Logical Framework (1991)
Formal deductive systems play an important role in computer science, particularly in the areas of logic and semantics of programming languages. They are employed in three different, but obviously...
Typing first-class continuations in ML (1991)
An extension of Standard ML with continuation primitives similar to those found in Scheme is considered. A number of alternative type systems are discussed, and several programming examples are...
Higher-Order Modules and the Phase Distinction (1990)
Robert Harper, John C. Mitchell, Eugenio Moggi
Typed λ-calculus is an important tool in programming language research because it provides an extensible framework for studying language features both in isolation and in their relation to...
Higher-Order Modules and the Phase Distinction (1990)
Robert Harper, John C. Mitchell, Eugenio Moggi
In earlier work, we used a typed function calculus, XML, with dependent types to analyze several aspects of the Standard ML type system. In this paper, we introduce a refinement of XML with a clear...
Higher-order Modules and the Phase Distinction (1990)
Robert Harper, John C. Mitchell
In earlier work, we used a typed function calculus, XML, with dependent types to analyze several as-pects of the Standard ML type system. In this pa-per, we introduce a refinement of XML with a clear...
A Framework for Defining Logics (1987)
Robert Harper, Furio Honsell, Gordon Plotkin
The Edinburgh Logical Framework (LF) provides a means to define (or present) logics. It is based on a general treatment of syntax, rules, and proofs by means of a typed -calculus with dependent...
Signatures for a Network Protocol Stack: A Systems Application of Standard ML
Edoardo Biagioni, Robert Harper, Peter Lee, Brian G. Milnes
Advanced programming languages such as Standard ML have rarely been used for systems programming tasks such as operating systems and network communications. In order to understand more fully the...
Typing First-Class Continuations in ML
Robert Harper, Bruce F. Duba, David Macqueen
An extension of ML with continuation primitives similar to those found in Scheme is considered. A number of alternative type systems are discussed, and several programming examples are given. A...
Typed Compilation of Recursive Datatypes
Joseph Vanderwaart Derek, Derek R. Dreyer, Leaf Petersen, Karl Crary, Robert Harper
Standard ML employs an opaque (or generative) semantics of datatype definitions, in which every datatype definition produces a new type that is di#erent from any other type, including other...
Typed Compilation of Recursive Datatypes
Joseph Vanderwaart Derek, Derek Dreyer, Leaf Petersen, Karl Crary, Robert Harper, Perry Cheng
Standard ML employs an opaque (or generative) semantics of datatypes, in which every datatype declaration produces a new type that is dierent from any other type, including other identically de ned...