Aleksey Nogin - Publications
[
2006|
2005|
2004|
2003|
2002|
2001|
2000|
1997|
1995|
online publications|
BibTeX]
-
![[New]](../images/new.gif)
Jason Hickey, Aleksey Nogin, Xin Yu, and Alexei Kopylov
Mechanized meta-reasoning using a hybrid
HOAS/de Bruijn representation and reflection.
In John H. Reppy and Julia L. Lawall, editors, Proceedings
of the 11th ACM SIGPLAN International Conference on Functional Programming,
ICFP 2006, pages 172–183. ACM, 2006.
-
Aleksey Nogin and Alexei Kopylov.
Formalizing type operations using the
“Image” type constructor.
In Proceedings of the 13th Workshop on Logic, Language,
Information and Computation (WoLLIC 2006), volume 165 of Electronic
Notes in Theoretical Computer Science, pages 121–132. Elsevier,
2006.
Extended version was submitted to Information and Computation
Journal.
-
Jason Hickey, Aleksey Nogin, Xin Yu, and Alexei Kopylov
Practical reflection for sequent logics.
In Proceedings of the International Workshop on Logical
Frameworks and Meta-Languages: Theory and Practice (LFMTP'06), Electronic
Notes in Theoretical Computer Science, 2006.
-
![[Updated]](../images/updated.gif)
Jason Hickey and Aleksey Nogin.
Formal Compiler Construction in a Logical
Framework.
Higher-Order and Symbolic Computation, 19(2–3):197–230, September 2006.
-
Jason Hickey and Aleksey Nogin.
OMake: Designing a scalable build
process.
In Luciano Baresi and Reiko Heckel, editors, Fundamental Approaches to
Software Engineering, 9th International Conference, FASE 2006, volume
3922 of Lecture Notes in Computer Science, pages 63–78. Springer,
2006.
An extended version is available as California Institute of
Technology technical report CaltechCSTR:2006.001.
-
Nathaniel Gray, Jason Hickey, Aleksey Nogin, and Cristian Tapus.
Building Extensible Compilers in a Formal Framework. A Formal Framework
User's Perspective.
In Konrad Slind, editor, Emerging Trends. Proceedings of the 17th
International Conference on Theorem Proving in Higher Order Logics (TPHOLs
2004), pages 57–70. University of Utah, 2004.
-
Cristian Tapus, Aleksey Nogin, Jason Hickey, and Jerome White.
A Simple Serializability Mechanism for a
Distributed Objects System.
In David A. Bader and Ashfaq A. Khokhar, editors,
Proceedings of the 17th International Conference on Parallel and
Distributed Computing Systems (PDCS-2004). International Society for
Computers and Their Applications (ISCA), 2004.
-
Jason Hickey and Aleksey Nogin.
Extensible Hierarchical Tactic Construction in
a Logical Framework.
In Konrad Slind, Annette Bunker, and Ganesh Gopalakrishnan, editors,
Proceedings of the 17th International Conference on Theorem Proving in
Higher Order Logics (TPHOLs 2004), volume 3223 of Lecture Notes in
Computer Science, pages 136–151. Springer-Verlag, 2004.
-
Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian E. Aydemir, Eli
Barzilay, Yegor Bryukhov, Richard Eaton, Adam Granicz, Alexei Kopylov,
Christoph Kreitz, Vladimir N. Krupski, Lori Lorigo, Stephan Schmitt, Carl
Witty, and Xin Yu.
MetaPRL — A Modular Logical
Environment.
In David Basin and Burkhart Wolff, editors, Proceedings of the 16th
International Conference on Theorem Proving in Higher Order Logics (TPHOLs
2003), volume 2758 of Lecture Notes in Computer Science, pages
287–303. Springer-Verlag, 2003.
-
Jason Hickey, Aleksey Nogin, Adam Granicz, and Brian Aydemir.
Compiler Implementation in a Formal Logical
Framework.
In Proceedings of the 2003 workshop on Mechanized reasoning about
languages with variable binding, pages 1–13. ACM Press, 2003.
-
Xin Yu, Aleksey Nogin, Alexei Kopylov, and Jason Hickey.
Formalizing Abstract Algebra in Type Theory
with Dependent Records.
In David Basin and Burkhart Wolff, editors, 16th International
Conference on Theorem Proving in Higher Order Logics (TPHOLs 2003). Emerging
Trends Proceedings, pages 13–27. Universität Freiburg, 2003.
-
Yegor Bryukhov, Alexei Kopylov, Vladimir Krupski, and Aleksey Nogin.
Implementing and Automating Basic Number Theory in
MetaPRL Proof Assistant.
In David Basin and Burkhart Wolff, editors, 16th International
Conference on Theorem Proving in Higher Order Logics (TPHOLs 2003). Emerging
Trends Proceedings, pages 29–39. Universität Freiburg, 2003.
-
Nathaniel Gray, Cristian Tapus, Aleksey Nogin, and Jason Hickey.
Building Reliable Compilers with a Formal
Methods Framework.
In Dr. Indrakshi Ray, editor, The 14th International Symposium on
Software Reliability Engineering (ISSRE 2003). Supplementary Proceeding,
pages 319–320. Chillarege Press, 2003.
- Aleksey Nogin.
Theory and Implementation of an Efficient Tactic-Based Logical
Framework.
Ph.D. Thesis, Cornell University. August 2002.
- Aleksey Nogin.
Quotient Types: A Modular Approach.
In Victor A. Carreño, Cézar A. Muñoz, and
Sophiène Tahar, editors, Proceedings of the 15th International
Conference on Theorem Proving in Higher Order Logics (TPHOLs 2002),
volume 2410 of Lecture Notes in Computer Science, pages 263–280.
Springer-Verlag, 2002.
- Aleksey Nogin and Jason Hickey.
Sequent Schema for Derived Rules.
In Victor A. Carreño, Cézar A. Muñoz, and
Sophiène Tahar, editors, Proceedings of the 15th International
Conference on Theorem Proving in Higher Order Logics (TPHOLs 2002),
volume 2410 of Lecture Notes in Computer Science, pages 281–297.
Springer-Verlag, 2002.
- Alexei Kopylov and Aleksey Nogin.
Markov's principle for propositional type
theory.
In L. Fribourg, editor, Computer Science Logic, Proceedings of
the 10th Annual Conference of the EACSL, volume 2142 of Lecture
Notes in Computer Science, pages 570-584. Springer-Verlag, 2001.
- Stephan Schmitt, Lori Lorigo, Christoph Kreitz, and Aleksey Nogin.
Jprover: Integrating connection-based theorem
proving into interactive proof assistants.
In International Joint Conference on Automated Reasoning,
volume 2083 of Lecture Notes in Artificial Intelligence, pages
421-426. Springer-Verlag, 2001.
- Jason J. Hickey and Aleksey Nogin.
Fast tactic-based theorem proving.
In J. Harrison and M. Aagaard, editors, Theorem Proving in
Higher Order Logics: 13th International Conference, TPHOLs 2000, volume 1869
of Lecture Notes in Computer Science, pages 252-266. Springer-Verlag, 2000.
- Aleksey Nogin.
Writing constructive proofs yielding efficient
extracted programs.
In Didier Galmiche, editor, Proceedings of the Workshop on
Type-Theoretic Languages: Proof Search and Semantics, volume 37 of
Electronic Notes in Theoretical Computer Science. Elsevier
Science Publishers, 2000
- Aleksey Nogin.
On Horn interpolation in linear logic.
Mathematical Logic and Theoretical Computer Science Prepublication
Series 1995-11, Steklov Mathematical Institute, April 1995.
In Russian.
Online Publications
- Jason Hickey, Aleksey Nogin, Alexei Kopylov, et al.
MetaPRL Home Page.
http://metaprl.org/
- Jason Hickey, Brian Aydemir, Yegor Bryukhov, Alexei Kopylov, Aleksey Nogin,
and Xin Yu.
A listing of MetaPRL theories.
http://metaprl.org/theories.pdf
- Jason Hickey, Nathaniel Gray, Aleksey Nogin, Cristian Tapus, and Xin Yu.
Introduction to MetaPRL Theorem Prover. Tutorial: Implementing FOL in
MetaPRL.
http://files.metaprl.org/papers/tutorial1.pdf
- Jason Hickey and Aleksey Nogin.
MetaPRL System Description
http://metaprl.org/system/default.html
- Jason Hickey, Aleksey Nogin and Alexei Kopylov.
MetaPRL User Guide.
http://metaprl.org/user-guide/default.html
- Aleksey Nogin and Vladimir Krupski.
MetaPRL Developer Guide.
http://metaprl.org/developer-guide/default.html
Back to the Home Page
Last update: Saturday, January 27, 2007 by Aleksey Nogin (e-mail: nogin+web@cs.caltech.edu)