Knowledge Base of
Publications,
Seminars,
& 
Math Library
PhD theses from the project are accessible at the NCSTRL web site.
Filter for: Aleksey Nogin
29 results
Formal Compiler Implementation in a Logical Framework
| cite »
by Jason Hickey, Aleksey Nogin
2003
MetaPRL -- A Modular Logical Environment
| cite »
by Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian Aydemir, Eli Barzilay, Lori Lorigo
2003
Quotient Types: A Modular Approach
| cite »
by Aleksey Nogin
2002
Review of Theorem Provers Outside Cornell part 2
by Aleksey Nogin
February 18, 2002
Review of Theorem Provers Outside Cornell part 1
by Aleksey Nogin
February 11, 2002
Is a type uniquely determined by its equivalence relation?
by Aleksey Nogin
November 26, 2001
Trip Report
by Aleksey Nogin
October 22, 2001
Markov's Principle for Propositional Type Theory
by Aleksey Nogin
August 20, 2001
JProver: Integrating Connection-Based Theorem Proving into Interactive Proof Assistants
| cite »
by Stephan Schmitt, Lori Lorigo, Christoph Kreitz, Aleksey Nogin
2001
Markov's Principle For Propositional Type Theory
| cite »
by Alexei Kopylov, Aleksey Nogin
2001
Writing Constructive Proofs Yielding Efficient Extracted Programs
| cite »
by Aleksey Nogin
2001
Modular approach to formalization of the quotient types
by Aleksey Nogin
April 23, 2001
Modular approach to quotient and other types
by Aleksey Nogin
April 16, 2001
New modular approach to formalizing complex types in type theory
by Aleksey Nogin
April 09, 2001
Internalizing proofs and provability
by Aleksey Nogin
February 19, 2001
A complete list of differences between MetaPRL and Nuprl 4 implementations of type theory (cont)
by Aleksey Nogin, Alexei Kopylov
December 04, 2000
A complete list of differences between MetaPRL and Nuprl 4 implementations of type theory
by Alexei Kopylov, Aleksey Nogin
November 27, 2000
Summer Reports
by Stuart F. Allen, Ralph Benzinger, Regina Barzilay, Ozan Hafizogullari, Aleksey Nogin, Amanda Holland-Minkley, Mark Bickford, Sasha Evfimievski, Lori Lorigo
September 18, 2000
Summer Reports
by Stuart F. Allen, Ralph Benzinger, Regina Barzilay, Ozan Hafizogullari, Aleksey Nogin, Amanda Holland-Minkley, Mark Bickford, Sasha Evfimievski, Lori Lorigo
September 11, 2000
Summer Reports
by Stuart F. Allen, Ralph Benzinger, Regina Barzilay, Ozan Hafizogullari, Aleksey Nogin, Amanda Holland-Minkley, Mark Bickford, Sasha Evfimievski, Lori Lorigo
September 04, 2000
Fast Tactic-Based Theorem Proving
| cite »
by Jason Hickey, Aleksey Nogin
2000
Differences between the MetaPRL type theory and the Nuprl type theory
by Aleksey Nogin
April 10, 2000
Efficient Programming by Extract in Nuprl Type Theory - Continued
by Aleksey Nogin
February 14, 2000
Efficient Programming by Extract in Nuprl Type Theory
by Aleksey Nogin
February 07, 2000
Intersections, Unions and Games
by Robert L. Constable, Alexei Kopylov, Aleksey Nogin
December 06, 1999
The Status of the Meta-Prl Project
by Aleksey Nogin
October 04, 1999
The Current Projects of the MetaPRL Group
by Aleksey Nogin, Jason Hickey
April 26, 1999
Speeding Up the MetaPRL Refiner
by Aleksey Nogin
February 08, 1999
Formal Models for Nuprl Evaluator
by Aleksey Nogin
March 24, 1998