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...
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...
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...
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,...
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...
Implementing and Automating Basic Number Theory in MetaPRL Proof Assistant ⋆ (2008)
Yegor Bryukhov, Alexei Kopylov, Vladimir Krupski, Aleksey Nogin
Abstract. No proof assistant can be considered complete unless it provides facilities for basic arithmetical reasoning. Indeed, integer theory is a part of the necessary foundation for most of...
Abstract Writing Constructive Proofs Yielding Efficient Extracted Programs (2008)
The NuPRL system [3] was designed for interactive writing of machine–checked constructive proofs and for extracting algorithms from the proofs. The extracted algorithms are guaranteed to be correct...
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...
Reliable Frameworks for Extensible Compilers (2008)
Jason Hickey Nathan, Nathan Gray, Aleksey Nogin, Cristian T Ăpus
on the use of a transformation logic defined within an existing general-purpose logical framework. We demonstrate how this methodology can be used to address several central issues in compiler design...
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...
On Dynamic Topological Logic of the Real Line (2008)
This article explores the topological interpretations of the modal language with two modalities—□, which is interpreted as the interior operation and ◯ (‘next’) which is...
Re ection and Propositions-as-Types (2007)
Sergei Artemov, Eli Barzilay, Robert L. Constable, Aleksey Nogin
Abstract. Re ection is the ability of a deductive system to internalize aspects of its own structure and thereby reason to some extent about itself. In this paper we present a theoretical framework...
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
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
Writing Constructive Proofs Yielding Ecient Extracted Programs (2007)
The NuPRL system [3] was designed for interactive writing of machine{checked constructive proofs and for extracting algorithms from the proofs. The extracted algorithms are guaranteed to be correct...
Stephan Schmitt, Lori Lorigo, Christoph Kreitz, Aleksey Nogin
Abstract. JProver is a rst-order intuitionistic theorem prover that creates sequent-style proof objects and can serve as a proof engine in interactive proof assistants with expressive constructive...
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...
Formalizing type operations using the “Image” type constructor (2006)
In this paper we introduce a new approach to formalizing certain type operations in type theory. Traditionally, many type constructors in type theory are independently axiomatized and the correctness...
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...
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
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...
Implementing and Automating Basic Number Theory In MetaPRL Proof Assistant (2003)
Yegor Bryukhov, Alexei Kopylov, Vladimir Krupski, Aleksey Nogin
No proof assistant can be considered complete unless it provides facilities for basic arithmetical reasoning. Indeed, integer theory is a part of the necessary foundation for most of mathematics,...
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...
Quotient Types --- a Modular Approach (2002)
In this paper we introduce a new approach to defining quotient types in type theory. We suggest replacing the existing monolithic rule set by a modular set of rules for a specially chosen set of...
Quotient Types --- a Modular Approach (2002)
In this paper we introduce a new approach to defining quotient types in type theory. We suggest replacing the existing monolithic rule set by a modular set of rules for a specially chosen set of...
JProver: Integrating connection-based theorem proving into interactive proof assistants (2001)
Stephan Schmitt, Lori Lorigo, Christoph Kreitz, Aleksey Nogin
Abstract. JProver is a first-order intuitionistic theorem prover that creates sequent-style proof objects and can serve as a proof engine in interactive proof assistants with expressive constructive...
Quotient types | a modular approach (2001)
riogincs. cornell. edu Abstract. In this paper we introduce a new approach to axiomatizing quotient types in type theory. We suggest replacing the existing monolithic rule set by a modular set of...
Quotient types | a modular approach (2001)
Abstract. In this paper we introduce a new approach to dening quotient types in type theory. We suggest replacing the existing monolithic rule set by a modular set of rules for a specially chosen set...
Markov’s principle for propositional type theory (2001)
Abstract. In this paper we show how to extend a constructive type theory with a principle that captures the spirit of Markov's principle from constructive recursive mathematics. Markov's...
Markov’s principle for propositional type theory (2001)
Abstract. In this paper we show how to extend a constructive type theory with a principle that captures the spirit of Markov's principle from constructive recursive mathematics. Markov's...
Quotient types | a modular approach (2001)
Abstract. In this paper we introduce a new approach to axiomatizing quotient types in type theory. We suggest replacing the existing monolithic rule set by a modular set of rules for a specially...
JProver: Integrating connection-based theorem proving into interactive proof assistants (2001)
Stephan Schmitt, Lori Lorigo, Christoph Kreitz, Aleksey Nogin
Abstract. JProver is a first-order intuitionistic theorem prover that creates sequent-style proof objects and can serve as a proof engine in interactive proof assistants with expressive constructive...
Quotient types | a modular approach (2001)
Abstract. In this paper we introduce a new approach to defining quotient types in type theory. We suggest replacing the existing monolithic rule set by a modular set of rules for a specially chosen...
Markov’s principle for propositional type theory (2001)
Abstract. In this paper we show how to extend a constructive type theory with a principle that captures the spirit of Markov’s principle from constructive recursive mathematics. Markov’s...
Quotient types | a modular approach (2001)
Abstract. In this paper we introduce a new approach to axiomatizing quotient types in type theory. We suggest replacing the existing monolithic rule set by a modular set of rules for a specially...
Markov’s principle for propositional type theory (2001)
Abstract. In this paper we show how to extend a constructive type theory with a principle that captures the spirit of Markov’s principle from constructive recursive mathematics. Markov’s...
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 implement automated proof search. Tactics use a general-purpose metalanguage to implement both general-purpose reasoning and...
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...
Improving the Efficiency of Nuprl Proofs (1997)
In order to use Nuprl system as a programming language with built-in verification one has to improve the efficiency of the programs extracted from the Nuprl proofs. In the current paper we consider...
Improving the Efficiency of Nuprl Proofs (1997)
In order to use Nuprl system as a programming language with built-in verification one has to improve the efficiency of the programs extracted from the Nuprl proofs. In the current paper we consider...
Improving the efficiency of Nuprl proofs (1997)
In order to use Nuprl system [1] as a programming language with builtin verification one has to improve the efficiency of the programs extracted from the Nuprl proofs. In the current paper we...
Improving the efficiency of Nuprl proofs (1997)
In order to use Nuprl system [1] as a programming language with builtin verification one has to improve the efficiency of the programs extracted from the Nuprl proofs. In the current paper we...