Abstract Dependent Intersection: A New Way of Defining Records in Type Theory (2008)
Record types are an important tool for programming and are essential in objectoriented calculi. Dependent record types are proven to be very useful for program specification and verification....
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,...
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...
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
Dependent Intersection: A New Way of Dening Records in Type Theory (2007)
Abstract. Record types are an important tool for programming and dependent record types are proven to be very useful for program speci-cation and verication. Unfortunately all known embedding of the...
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...
Type Theoretical Foundations for Data Structures, Classes, and Objects (2004)
In this thesis we explore the question of how to represent programming data structures in a constructive type theory. The basic data structures in programing languages are records and objects. Most...
Type Theoretical Foundations for Data Structures, Classes, and Objects (2004)
In this thesis we explore the question of how to represent programming data structures in a constructive type theory. The basic data structures in programing languages are records and objects. Most...
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,...
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...
Dependent intersection: A new way of defining records in type theory (2003)
Records and dependent records are a powerful tool for programming, representing mathematical concepts, and program verification. In the last decade several type systems with records as primitive...
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...
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...
Dependent Intersection: A New Way of Defining Records in Type Theory (2000)
Record types are an important tool for programming and dependent record types are proven to be very useful for program specification and verification. Unfortunately all known embedding of the...
Dependent Intersection: A New Way of Defining Records in Type Theory (2000)
Record types are an important tool for programming and dependent record types are proven to be very useful for program specification and verification. Unfortunately all known embedding of the...
Dependent intersection: A new way of defining records in type theory (2000)
Records and dependent records are a powerful tool for programming, representing mathematical concepts, and program verification. In the last decade several type systems with records as primitive...