MetaPRL-related Publications
The list of papers is currently under construction and could be somewhat
incomplete.
[
2004|
2003|
2002|
2001|
2000|
1999|
1997|
online publications|
BibTeX]
- 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). Sumpplementary Proceeding,
pages 319–320. Chillarege 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.
- 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.
- 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.
- Alexei Kopylov.
Dependent Intersection: A New Way of Defining
Records in Type Theory.
In Proceedings of 18th IEEE Symposium on Logic in Computer Science (LICS),
pages 86–95, IEEE Computer Society 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.
- Brian Aydemir, Adam Granicz, and Jason Hickey.
Formal Design Environments.
Theorem Proving in Higher-Order Logics (TPHOLs), 2002. Appears in NASA
technical report NASA/CP-2002-211736.
- 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.
- Jason Hickey.
Fault-Tolerant Distributed Theorem
Proving.
In Harald Ganzinger, editor, Proceedings of the 16th International
Conference on Automated Deduction, volume 1632 of Lecture Notes in
Artificial Intelligence, pages 227–231, July 7–10 1999.
Online Publications