#
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