@string{ LNCS = "Lecture Notes in Computer Science" }
@string{ LNAI = "Lecture Notes in Artificial Intelligence" }
@preamble{ \def\MetaPRL{\textsf{MetaPRL}} }
@preamble{ \def\JProver{\textsf{JProver}} }
@InProceedings{BKKN03,
AUTHOR = {Yegor Bryukhov and Alexei Kopylov and Vladimir Krupski and Aleksey Nogin},
TITLE = {Implementing and Automating Basic Number Theory in {\MetaPRL} Proof Assistant},
PAGES = {29--39},
CROSSREF = {tphols2003b}
}
@InProceedings{GTNH03,
Author = {Nathaniel Gray and Cristian Tapus and Aleksey Nogin and Jason Hickey},
Title = {Building Reliable Compilers with a Formal Methods Framework},
Pages = {319--320},
Publisher = {Chillarege Press},
BookTitle = {The 14$^{th}$ International Symposium on Software Reliability Engineering (ISSRE 2003). Sumpplementary Proceedings},
Editor = {Dr. Indrakshi Ray},
Year = 2003
}
@inproceedings{HN00,
crossref = "tphols2000",
title = "Fast Tactic-based Theorem Proving",
author = "Jason J. Hickey and Aleksey Nogin",
pages = "252--266"
}
@InProceedings{Hic99b,
author = {Hickey, Jason J.},
title = {Fault-Tolerant Distributed Theorem Proving},
pages = {227--231},
crossref = {CADE99}
}
@inproceedings{KN01,
author = "Alexei Kopylov and Aleksey Nogin",
title = "Markov's Principle for Propositional Type Theory",
pages = "570--584",
crossref = "CSL01",
note = ""
}
@InProceedings{HNC+03,
author = {Jason Hickey and Aleksey Nogin and Robert L. Constable and Brian E. Aydemir and Eli Barzilay and Yegor Bryukhov and Richard Eaton and Adam Granicz and Alexei Kopylov and Christoph Kreitz and Vladimir N. Krupski and Lori Lorigo and Stephan Schmitt and Carl Witty and Xin Yu},
title = {{\MetaPRL} --- {A} Modular Logical Environment},
pages = {287--303},
crossref = {tphols2003}
}
@inproceedings{HNGA03,
author = {Jason Hickey and Aleksey Nogin and Adam Granicz and Brian Aydemir},
title = {Compiler implementation in a formal logical framework},
booktitle = {Proceedings of the 2003 workshop on {M}echanized reasoning about languages with variable binding},
year = 2003,
isbn = {1-58113-800-8/03/0008},
pages = {1--13},
location = {Uppsala, Sweden},
doi = {http://doi.acm.org/10.1145/976571.976575},
note = {\url{http://doi.acm.org/10.1145/976571.976575}},
url = {http://doi.acm.org/10.1145/976571.976575},
publisher = {ACM Press},
}
@inproceedings{NH02,
author = "Aleksey Nogin and Jason Hickey",
title = "Sequent Schema for Derived Rules",
pages = "281--297",
crossref = "tphols2002",
note = "See also \url{http://nogin.org/papers/derived_rules.html}"
}
@Techreport{Nog02a,
author = "Aleksey Nogin",
title = "Quotient Types --- A Modular Approach",
institution = "Cornell University",
type = "Department of Computer Science",
number = "\href{http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR2002-1869}{TR2002-1869}",
month = "April",
year = 2002,
note = "See also \url{http://nogin.org/papers/quotients.html}"
}
@INPROCEEDINGS{Nog02b,
author = "Aleksey Nogin",
title = "Quotient Types: A Modular Approach",
pages = "263--280",
crossref = "tphols2002",
note = "Available at \url{http://nogin.org/papers/quotients.html}"
}
@PhdThesis{Nog02c,
author = "Aleksey Nogin",
title = "Theory and Implementation of an Efficient Tactic-Based Logical Framework",
school = "Cornell University",
address = "Ithaca, NY",
month = aug,
year = 2002
}
@inproceedings{SLKN01,
author = "Stephan Schmitt and Lori Lorigo and Christoph Kreitz and Aleksey Nogin",
title = "{\JProver}: Integrating Connection-Based Theorem Proving into Interactive Proof Assistants",
booktitle = "International Joint Conference on Automated Reasoning",
series = LNAI,
volume = 2083,
pages = "421--426",
publisher = "Springer-Verlag",
year = 2001
}
@InProceedings{YNKH03,
AUTHOR = {Xin Yu and Aleksey Nogin and Alexei Kopylov and Jason Hickey},
TITLE = {Formalizing Abstract Algebra in Type Theory with Dependent Records},
PAGES = {13--27},
CROSSREF = {tphols2003b},
NOTE = {\url{http://nogin.org/papers/formalaa.html}},
}
@Misc{MPHome,
author = "Jason J. Hickey and Aleksey Nogin and Alexei Kopylov and others",
key = "MetaPRL",
title = "{\MetaPRL} Home Page",
note = "\url{http://metaprl.org/}"
}
@Misc{MPthe,
author = "Jason J. Hickey and Brian Aydemir and Yegor Bryukhov and Alexei Kopylov and Aleksey Nogin and Xin Yu",
title = "A Listing of {\MetaPRL} Theories",
note = "\url{http://metaprl.org/theories.pdf}"
}
@Proceedings{CADE99,
title = {Proceedings of the 16$^{th}$ International Conference on
Automated Deduction},
booktitle = {Proceedings of the 16$^{th}$ International Conference on
Automated Deduction},
editor = {Harald Ganzinger},
volume = 1632,
series = LNAI,
year = 1999,
publisher = {Trento, Italy},
address = {Berlin},
month = {July 7--10},
ISBN = {3-540-66222-7}
}
@proceedings{CSL01,
booktitle = "Computer Science Logic, Proceedings of the 10$^{th}$ Annual Conference of the EACSL",
title = "Computer Science Logic, Proceedings of the 10$^{th}$ Annual Conference of the EACSL",
volume = "2142",
series = LNCS,
editor = "L. Fribourg",
publisher = "Springer-Verlag",
year = "2001",
note = "\url{http://link.springer-ny.com/link/service/series/0558/tocs/t2142.htm}"
}
@PROCEEDINGS{tphols2000,
key = "TPHOLs00",
title = "Theorem Proving in Higher Order Logics: 13$^{th}$ International Conference, TPHOLs 2000",
editor = "J. Harrison and M. Aagaard",
booktitle = "Theorem Proving in Higher Order Logics: 13$^{th}$ International Conference, TPHOLs 2000",
series = LNCS,
volume = 1869,
year = 2000,
publisher = "Springer-Verlag",
}
@Proceedings{tphols2002,
key = {TPHOLs02},
title = {Proceedings of the 15$^{th}$ International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2002)},
booktitle = {Proceedings of the 15$^{th}$ International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2002)},
series = LNCS,
volume = 2410,
editor = {Victor A. Carre{\~n}o and C{\'e}zar A. Mu{\~n}oz and Sophi{\`e}ne Tahar},
publisher = {Springer-Verlag},
year = 2002,
}
@Proceedings{tphols2003,
key = {TPHOLs03},
title = {Proceedings of the 16$^{th}$ International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2003)},
booktitle = {Proceedings of the 16$^{th}$ International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2003)},
series = LNCS,
volume = 2758,
editor = {David Basin and Burkhart Wolff},
publisher = {Springer-Verlag},
year = 2003,
}
@PROCEEDINGS{tphols2003b,
KEY = {TPHOLs03B},
TITLE = {16$^{th}$ International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2003). Emerging Trends Proceedings},
BOOKTITLE = {16$^{th}$ International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2003). Emerging Trends Proceedings},
EDITOR = {David Basin and Burkhart Wolff},
PUBLISHER = {Universit{\"a}t Freiburg},
YEAR = 2003,
}