X.: MetaPRL — A modular logical environment (2009)
Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian E. Aydemir, Yegor Bryukhov, Richard Eaton, ...
Abstract. MetaPRL is the latest system to come out of over twenty five years of research by the Cornell PRL group. While initially created at Cornell, MetaPRL is currently a collaborative project...
Robert L. Constable, Jason Hickey
Abstract This article presents a theory of classes and inheritance built on top of constructive typetheory. Classes are defined using dependent and very dependent function types that are found in the...
Building Extensible Compilers in a Formal Framework ⋆ A Formal Framework User’s Perspective (2009)
Nathaniel Gray, Jason Hickey, Aleksey Nogin, Cristian T Ăpu¸s
Abstract. We outline a new methodology for compiler design, based on the use of a transformation logic defined within an existing generalpurpose logical framework. We discuss how this methodology can...
Ţăpuş, Cristian, Hickey, Jason
This paper examines the use of speculations, a form of distributed transactions, for improving the reliability and fault tolerance of distributed systems. A speculation is defined as a computation...
Process Migration and Transactions Using a Formal Intermediate Language ∗ ABSTRACT (2008)
Jason Hickey, Justin D. Smith, Brian Aydemir, Nathaniel Gray, Adam Granicz, Cristian T Ăpus
Process migration and atomic transactions are essential tools for constructing fault-tolerant distributed systems. Process migration provides location transparency, the ability to perform...
A Mechanism for Sequential Consistency in a Distributed Objects System (2008)
Cristian T Ăpu¸s, Aleksey Nogin, Jason Hickey, Jerome White
This paper presents a new protocol for ensuring sequential consistency in a distributed objects system. The protocol is efficient and simple. In addition to providing a high-level overview of the...
A Mechanism for Sequential Consistency in a Distributed Objects System (2008)
Cristian T Ăpu¸s, Aleksey Nogin, Jason Hickey, Jerome White
This paper presents a new protocol for ensuring sequential consistency in a distributed objects system. The protocol is efficient and simple. In addition to providing a high-level overview of the...
Dutch Government, Jason Hickey
• Co-author of the KOA Vote Counting System, with Engelbert Hubbers and Martijn Oostdijk, for the
DRAFT. DO NOT REDISTRIBUTE. (2008)
Jason Hickey, Copyright Jason Hickey
This book has been submitted for publication by Cambridge University Press.
Formal Design Environments (2008)
Brian Aydemir, Adam Granicz, Jason Hickey
Abstract. We present the design of a formal integrated design environment. The long-term goal of this effort is to allow seamless interaction between software production tools and formal design and...
Ken Birman, Bob Constable, Mark Hayden, Jason Hickey, Christoph Kreitz, Robbert Van Renesse, ...
multi-year Cornell research program in process group communication used for fault-tolerance, security and adaptation. Our intent was to understand the degree to which a single system could offer...
LFMTP 2006 Practical Reflection for Sequent Logics (2008)
Jason Hickey, Aleksey Nogin, Xin Yu, Alexei Kopylov
It is well-known that adding reflective reasoning can tremendously increase the power of a proof assistant. In order for this theoretical increase of power to become accessible to users in practice,...
Adam Granicz, Daniel M. Zimmerman, Jason Hickey
Abstract. In this paper we describe the implementation of the UNITY formalism as an extension of general-purpose languages and show its translation to C abstract syntax using Phobos, our generic...
Abstract. The task of designing and implementing a compiler can be a difficult and error-prone process. In this paper, we present a new approach based on the use of higher-order abstract syntax and...
Ken Birman, Bob Constable, Mark Hayden, Jason Hickey, Christoph Kreitz, Robbert Van Renesse, ...
Abstract – The Horus and Ensemble efforts culminated a multi-year Cornell research program in process group communication used for fault-tolerance, security and adaptation. Our intent was to...
Steps Toward a World Wide Digital Library of Formal Algorithmic Knowledge (2008)
Robert L. Constable, Stuart Allen, Mark Bickford, James Caldwell, Jason Hickey, Christoph Kreitz
Formal Compiler Construction (2008)
In Logical Framework, Jason Hickey, Aleksey Nogin
The task of designing and implementing a compiler can be a di#cult and error-prone process. In this paper, we present a new approach based on the use of higher-order abstract syntax and term...
A Mechanism for Sequential Consistency in a (2008)
Distributed Objects System, Cristian T Ăpu¸s, Aleksey Nogin, Jason Hickey, Jerome White
This paper presents a new protocol for ensuring sequential consistency in a distributed objects system. The protocol is e#cient and simple. In addition to providing a high-level overview of the...
Johnny Chen, Eleni Drinea, Seth Gilbert, M. T. Hajiaghayi, Jason Hickey, Rebecca Hitchcock, ...
Grant Wang, and David Woodru for scribing these lectures. Thanks to Dan Spielman for lecturing on March 13, 2002; and most signicantly for providing the material for the course from prior semesters....
Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian E. Aydemir, Yegor Bryukhov, Richard Eaton, ...
, Christoph Kreitz 2, Vladimir N. Krupski 4, Lori Lorigo 2, Stephan Schmitt 5, Carl Witty
Jason Frantz, Cristian T Ăpu¸s, Justin D. Smith, Jason Hickey
MojaveFS is a key component of an infrastructure supporting dis-tributed transactional computing. It is closely tied to the Mojave Com-piler Collection, which provides high-level programming language...
Adam Granicz, Daniel M. Zimmerman, Jason Hickey
Abstract. In this paper we describe the implementation of the UNITY formalism as an extension of general-purpose languages and show its translation to C abstract syntax using Phobos, our generic...
A Listing of MetaPRL Theories 1 (2007)
Jason Hickey, Brian Aydemir, Yegor Bryukhov, Alexei Kopylov, Aleksey Nogin, Xin Yu
This document contains a listing of most of the MetaPRL logical theories. It is generated automatically on a daily basis. To get the latest version, go to
Adam Granicz, Daniel M. Zimmerman, Jason Hickey
Abstract. In this paper we describe the implementation of the UNITY formalism as an extension of general-purpose languages and show its translation to C abstract syntax using Phobos, our generic...
CDC02-REG1035 The Caltech Multi-Vehicle Wireless Testbed 1 (2007)
Lars Cremean, William B. Dunbar, Dave Van Gogh, Jason Hickey, Eric Klavins, Jason Meltzer, ...
Abstract: In this paper we introduce the Caltech Multi-Vehicle Wireless Testbed (MVWT), a platform for testing decentralized control methodologies for multiple vehicle coordination and formation...
Formal Design Environments (2007)
Brian Aydemir, Adam Granicz, Jason Hickey
Abstract. We present the design of a formal integrated design environment. The long-term goal of this eort is to allow seamless interaction between software production tools and formal design and...
John Doyle, Michelle Effros, Jason Hickey, Steven Low
We plan to build a testbed consisting of 8-10 mobile vehicles with embedded computing and communications capability for use in testing new approaches for command and control across dynamic networks....
Jason Hickey, Nancy Lynch, Robbert Van Renesse
Abstract. Ensemble is a widely used group communication system that supports distributed programming by providing precise guarantees for synchronization, message ordering, and message delivery....
A theory of nested speculative execution (2007)
Abstract. Implementing distributed applications is a challenging task. Developers of such systems are confronted with issues like fault-tolerance, efficient synchronization mechanisms, and the...
OMake: Designing a Scalable Build Process (2006)
Modern software codebases are frequently large, heterogeneous, and constantly evolving. The languages and tools for software construction, including code builds and configuration management, have not...
OMake: Designing a scalable build process (2006)
Abstract. Modern software codebases are frequently large, heterogeneous, and constantly evolving. The languages and tools for software construction, including code builds and configuration...
OMake: Designing a scalable build process (2006)
Abstract. Modern software codebases are frequently large, heterogeneous, andconstantly evolving. The languages and tools for software construction, including code builds and configuration management,...
OMake: Designing a scalable build process (2006)
Abstract. Modern software codebases are frequently large, heterogeneous, andconstantly evolving. The languages and tools for software construction, including code builds and configuration management,...
OMake: Designing a scalable build process (2006)
Abstract. Modern software codebases are frequently large, heterogeneous, and constantly evolving. The languages and tools for software construction, including code builds and configuration...
OMake: Designing a scalable build process (2006)
Abstract. Modern software codebases are frequently large, heterogeneous, and constantly evolving. The languages and tools for software construction, including code builds and configuration...
A Listing of MetaPRL Theories 1 (2006)
Jason Hickey, Brian Aydemir, Yegor Bryukhov, Alexei Kopylov, Aleksey Nogin, Xin Yu
This document contains a listing of most of the MetaPRL logical theories. It is generated automatically on a daily basis. To get the latest version, go to
A Computational Approach to Reflective Meta-Reasoning about Languages with Bindings (2005)
Nogin, Aleksey, Kopylov, Alexei, Xin, Yu, Hickey, Jason
We present a foundation for a computational meta-theory of languages with bindings implemented in a computer-aided formal reasoning environment. Our theory provides the ability to reason abstractly...
A Computational Approach to Reflective Meta-Reasoning about Languages with Bindings (2005)
Aleksey Nogin, Alexei Kopylov, Xin Yu, Jason Hickey
We present a foundation for a computational meta-theory of languages with bindings implemented in a computer-aided formal reasoning environment. Our theory provides the ability to reason abstractly...
A Computational Approach to Reflective Meta-Reasoning about Languages with Bindings (2005)
Aleksey Nogin, Alexei Kopylov, Xin Yu, Jason Hickey
We present a foundation for a computational meta-theory of languages with bindings implemented in a computer-aided formal reasoning environment. Our theory provides the ability to reason abstractly...
A Computational Approach to Reflective Meta-Reasoning about Languages with Bindings (2005)
Aleksey Nogin, Alexei Kopylov, Xin Yu, Jason Hickey
We present a foundation for a computational meta-theory of languages with bindings implemented in a computer-aided formal reasoning environment. Our theory provides the ability to reason abstractly...
A computational approach to reflective meta-reasoning about languages with bindings (2005)
Aleksey Nogin, Alexei Kopylov, Xin Yu, Jason Hickey
We present a foundation for a computational meta-theory of languages with bindings implemented in a computer-aided formal reasoning environment. Our theory provides the ability to reason abstractly...
Extensible Hierarchical Tactic Construction in a (2004)
Logical Framework Jason, Jason Hickey, Aleksey Nogin
Theorem provers for higher-order logics often use tactics to implement automated proof search. Often some basic tactics are designed to behave very di#erently in di#erent contexts. Even in a prover...
Abstract. Theorem provers for higher-order logics often use tactics to implement automated proof search. Often some basic tactics are designed to behave very differently in different contexts. Even...
Formal Compiler Implementation in a Logical Framework (2003)
Hickey, Jason, Nogin, Aleksey, Granicz, Adam, Aydemir, Brian
The task of designing and implementing a compiler can be a dicult and error-prone process. In this paper, we present a new approach based on the use of higher-order abstract syntax and term rewriting...
Formalizing Abstract Algebra in Constructive Set Theory (2003)
We present a machine-checked formalization of elementary abstract algebra in constructive set theory. Our formalization uses an approach where we start by specifying the group axioms as a collection...
Building reliable compilers with a formal methods framework (2003)
Nathaniel Gray, Cristian T Apus, Aleksey Nogin, Jason Hickey
Reliability is an issue in compiler writing just like it is in any other type of large software endeavor. Compiler reliability is particularly important, however, because compilers
Kernel level speculative DSM (2003)
Cristian T Ăpu¸s, Justin D. Smith, Jason Hickey
Keywords: distributed shared memory, speculation, Mojave. Interprocess communication (IPC) is ubiquitous in today’s computing world. One of the simplest mechanisms for IPC is shared memory. We...
Kernel level speculative DSM (2003)
Cristian T Ăpus, Justin D. Smith, Jason Hickey
Interprocess communication (IPC) is ubiquitous in today’s computing world. One of the simplest mechanisms for IPC is shared memory. We present a system that enhances the System V IPC API to support...
Formal compiler implementation in a logical framework (2003)
Jason Hickey, Aleksey Nogin, Adam Granicz, Brian Aydemir
The task of designing and implementing a compiler can be a dicult and error-prone process. In this paper, we present syntax and term rewriting in a logical framework. All program transformations,...
Formal compiler implementation in a logical framework (2003)
Jason Hickey, Aleksey Nogin, Adam Granicz, Brian Aydemir
The task of designing and implementing a compiler can be a dicult and error-prone process. In this paper, we present a new approach based on the use of higher-order abstract syntax and term rewriting...
Formal Compiler Implementation in a Logical Framework (2003)
Jason Hickey, Aleksey Nogin, Adam Granicz, Brian Aydemir
The task of designing and implementing a compiler can be a difficult and error-prone process. In this paper, we present a new approach based on the use of higher-order abstract syntax and term...
Compiler Implementation in a Formal Logical Framework (2003)
Jason Hickey, Aleksey Nogin, Adam Granicz, Brian Aydemir
The task of designing and implementing a compiler can be a dicult and error-prone process. In this paper, we present a new approach based on the use of higher-order abstract syntax and term rewriting...
Building Reliable Compilers with a Formal Methods Framework (2003)
Nathaniel Gray Cristian, Cristian T Ăpus, Aleksey Nogin, Jason Hickey
this paper we describe an ongoing research effort to address these problems by building a compiler within the MetaPRL formal programming environment [1]. Working with MetaPRL allows us to write the...
MetaPRL — A Modular Logical Environment (2003)
Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian E. Aydemir, Yegor Bryukhov, Richard Eaton, ...
Abstract. MetaPRL is the latest system to come out of over twenty five years of research by the Cornell PRL group. While initially created at Cornell, MetaPRL is currently a collaborative project...
Compiler implementation in a formal logical framework (2003)
Jason Hickey, Aleksey Nogin, Adam Granicz, Brian Aydemir
The task of designing and implementing a compiler can be a difficult and error-prone process. In this paper, we present syntax and term rewriting in a logical framework. All program transformations,...
Building reliable compilers with a formal methods framework (2003)
Nathaniel Gray, Cristian T Ăpus, Aleksey Nogin, Jason Hickey
Reliability is an issue in compiler writing just like it is in
MetaPRL — A Modular Logical Environment (2003)
Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian E. Aydemir, Yegor Bryukhov, Richard Eaton, ...
Abstract. MetaPRL is the latest system to come out of over twenty five years of research by the Cornell PRL group. While initially created at Cornell, MetaPRL is currently a collaborative project...
Formalizing Abstract Algebra in Type Theory with Dependent Records (2003)
Xin Yu, Aleksey Nogin, Alexei Kopylov, Jason Hickey
algebra suitable for a general reasoning. One of the most common ways to formalize abstract algebra is to make use of a module system to specify an algebra as a theory. However, this approach suffers...
Phobos: A front-end approach to extensible compilers (long version) (2002)
This paper describes a practical approach for implementing certain types of domain-specific languages with extensible compilers. Given a compiler with one or more front-end languages, we introduce...
Process Migration and Transactions Using a Novel Intermediate Language (2002)
Hickey, Jason, Smith, Justin D., Aydemir, Brian, Gray, Nathaniel, Granicz, Adam, Tapus, Cristian
Phobos: A front-end approach to extensible compilers (2002)
Abstract. This paper describes a practical approach for implementing certain types of domain-specific languages with extensible compilers. Given a compiler with one or more front-end languages, we...
Phobos: A front-end approach to extensible compilers (2002)
Phobos: A front-end approach to extensible compilers Abstract. This paper describes a practical approach for implementing certain types of domain-specific languages with extensible compilers. Given a...
Process migration and transactions using a novel intermediate language (2002)
Jason Hickey, Justin D. Smith, Brian Aydemir, Nathaniel Gray, Adam Granicz, Cristian Tapus
Process migration and atomic transactions are essential tools for constructing fault-tolerant distributed systems. We present a new system that includes a typed intermediate language and runtime...
The Caltech Multi-Vehicle Wireless Testbed (2002)
Lars Cremean, William B. Dunbar, Dave Van Gogh, Jason Hickey, Eric Klavins, Jason Meltzer, ...
Abstract: In this paper we introduce the Caltech Multi-Vehicle Wireless Testbed (MVWT), a platform for testing decentralized control methodologies for multiple vehicle coordination and formation...
Robustness and the Internet: Theoretical Foundations (2002)
John C. Doyle, Jean Carlson, Steven H. Low, Fernando Paganini, Glenn Vinnicombe, Walter Willinger, ...
This article uses the Internet as a starting point to illustrate universal aspects of complex systems throughout technology and biology. Complexity in most systems is driven by the need for...
Fast tactic-based theorem proving (2000)
Abstract. Theorem provers for higher-order logics often use tactics to implement automated proof search. Tactics use a general-purpose metalanguage to implement both general-purpose reasoning and...
Fast tactic-based theorem proving (2000)
Abstract. Theorem provers for higher-order logics often use tactics to implement automated proof search. Tactics use a general-purpose metalanguage to implement both general-purpose reasoning and...
Fast Tactic-based Theorem Proving (2000)
Theorem provers for higher-order logics often use tactics to implement automated proof search. Tactics use a general-purpose meta-language to implement both general-purpose reasoning and...
Fast tactic-based theorem proving (2000)
Abstract. Theorem provers for higher-order logics often use tactics to code automated proof search. Tactics use a procedural meta-language to perform both algorithmic and heuristic proof search, as...
Fast tactic-based theorem proving (2000)
Abstract. Theorem provers for higher-order logics often use tactics to implement automated proof search. Tactics use a general-purpose metalanguage to implement both general-purpose reasoning and...
NuPRL’s class theory and its applications (2000)
Robert L. Constable, Jason Hickey
This article presents a theory of classes and inheritance built on top of constructive type theory. Classes are defined using dependent and very dependent function types that are found in the Nuprl...
The Horus and Ensemble Projects: Accomplishments and Limitations (1999)
Birman, Kenneth P., Constable, Robert, Hayden, Mark, Hickey, Jason, Kreitz, Christoph, Van Renesse, Robbert, ...
The Horus and Ensemble efforts culminated a multi-year Cornell research program in process group communication used for fault-tolerance, security and adaptation. Our intent was to understand the...
The Horus and Ensemble Projects: Accomplishments and Limitations (1999)
Birman, Kenneth P., Constable, Robert, Hayden, Mark, Hickey, Jason, Kreitz, Christoph, Van Renesse, Robbert, ...
The Horus and Ensemble efforts culminated a multi-year Cornell research program in process group communication used for fault-tolerance, security and adaptation. Our intent was to understand the...
Predicate transformers for infinite-state automata in nuprl type theory (1999)
This paper has two goals. The first is to present a formalization in Nuprl type theory of a very general methodology for system description, specification and verification. The method is especially...
Specifications and proofs for Ensemble Layers (1999)
Jason Hickey, Nancy Lynch, Robbert Van Renesse
Ensemble is a widely used group communication system that supports distributed programming by providing precise guarantees for synchronization, message ordering, and message delivery. Ensemble eases...
Building Reliable, High-Performance Communication Systems from Components (1999)
Xiaoming Liu, Christoph Kreitz, Robbert Van Renesse, Jason Hickey
Although building systems from components has attractions, this approach also has problems. Can we be sure that a certain configuration of components is correct? Can it perform as well as a...
An Object-Oriented Approach to Verifying Group Communication Systems (1999)
. Group communication system assist the development of faulttolerant distributed algorithms by providing precise guarantees on message ordering, delivery, and synchronization. Ensemble is a widely...
Fault-Tolerant Distributed Theorem Proving (1999)
Higher-order logics are expressive tools for tasks ranging from formalizing the foundations of mathematics to large-scale software verification and synthesis. Because of their complexity, proofs in...
Building Reliable, High-Performance Communication Systems From Components (1999)
Xiaoming Liu, Christoph Kreitz, Robbert Van Renesse, Jason Hickey, Mark Hayden, Kenneth Birman, ...
Although building systems from components has attractions, this approach also has problems. Can we be sure that a certain configuration of components is correct? Can it perform as well as a...
Fault-tolerant distributed theorem proving (1999)
Abstract. Higher-order logics are expressive tools for tasks ranging from formalizing the foundations of mathematics to large-scale software veri cation and synthesis. Because of their complexity,...
Xiaoming Liu, Christoph Kreitz, Robbert Van Renesse, Jason Hickey
Although building systems from components has attractions, this approach also has problems. Can we be sure that a certain configuration of components is correct? Can it perform as well as a...
Building reliable, high-performance communication systems from components (1999)
Xiaoming Liu, Christoph Kreitz, Robbert Van Renesse, Jason Hickey, Mark Hayden, Kenneth Birman, ...
Although building systems from components has attractions, this approach also has problems. Can we be sure that a certain configuration of components is correct? Can it perform as well as a...
Birman, Ken, Constable, Bob, Hayden, Mark, Hickey, Jason, Kreitz, Christoph
The Horus and Ensemble efforts culminated a multi-year Cornell research program in process group communication used for fault-tolerance, security and adaptation. The intent was to understand the...
A Multi-Vehicles, Wireless Testbed for Networked Control, Communications and Computing (1998)
Murray, Richard, Doyle, John, Effros, Michelle, Hickey, Jason, Low, Steven
We have constructed a testbed consisting of 4 mobile vehicles (with 4 additional vehicles being completed), each with embedded computing and communications capability for use in testing new...
High Confidence Reconfigurable Distributed Control (1998)
Hickey, Jason, Hauser, John, Murray, Richard
The Caltech/Colorado SEC project developed and tested two major advances in software enabled control: optimization-based control using real-time trajectory generation and logical programming...
High Confidence Reconfigurable Distributed Control (1998)
Hickey, Jason, Hauser, John, Murray, Richard
The Caltech/Colorado SEC project developed and tested two major advances in software enabled control: optimization-based control using real-time trajectory generation and logical programming...
Formal Compiler Implementation in a Logical Framework (1998)
Hickey, Jason, Nogin, Aleksey, Granicz, Adam, Aydemir, Brian
The task of designing and implementing a compiler can be a difficult and error-prone process. In this paper, we present a new approach based on the use of higher-order abstract syntax and term...
An object-oriented approach to verifying group communication systems (1998)
Group communication system assist the development of fault-tolerant distributed algorithms by providing precise guarantees on message ordering, delivery, and synchronization. Ensemble is a widely...
A Proof Environment for the Development of Group Communication Systems (1998)
Christoph Kreitz, Mark Hayden, Jason Hickey, H. Kirchner
We present a theorem proving environment for the development of reliable and efficient group communication systems. Our approach makes methods of automated deduction applicable to the implementation...
A proof environment for the development of group communication systems (1998)
Christoph Kreitz, Mark Hayden, Jason Hickey
Abstract. We present a theorem proving environment for the development of reliable and efficient group communication systems. Our approach makes methods of automated deduction applicable to the...
A proof environment for the development of group communication systems (1998)
Christoph Kreitz, Mark Hayden, Jason Hickey
Abstract. We present a theorem proving environment for the development of reliable and efficient group communication systems. Our approach makes methods of automated deduction applicable to the...
Thesis: Distributed Speculations: Providing Fault-tolerance and Improving Performance (1995)
Cristian T Ăpu¸s, Advisor Professor, Jason Hickey
March 1997- July 1997, Lille, France, as winner of TEMPUS scholarship (GPA 18 out of 20)
Non-restoring integer square root: A case study in design by principled optimization (1994)
Miriam Leeser, Jason Hickey, Mark Aagaard
Abstract. Theorem proving techniques are particularly well suited for reasoning about arithmetic above the bit level and for relating different levels of abstraction. In this paper we show how a...
Non-restoring integer square root: A case study in design by principled optimization (1994)
Miriam Leeser, Jason Hickey, Mark Aagaard
Abstract. Theorem proving techniques are particularly well suited for reasoning about arithmetic above the bit level and for relating di erent levels of abstraction. In this paper we show how a...