@string{ LNCS = "Lecture Notes in Computer Science" }
@string{ LNAI = "Lecture Notes in Artificial Intelligence" }
@preamble{ \def\OMake{\textsf{OMake}} }
@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). Supplementary Proceedings},
Editor = {Dr. Indrakshi Ray},
Year = 2003
}
@InProceedings{GHNT04,
Author = {Nathaniel Gray and Jason Hickey and Aleksey Nogin and Cristian Tapus},
Title = {Building Extensible Compilers in a Formal Framework. {A} Formal Framework User's Perspective},
Crossref = {tphols2004b},
Pages = {57--70},
URL = {http://nogin.org/papers/mmc-tphols.html}
}
@inproceedings{HN00,
crossref = "tphols2000",
title = "Fast Tactic-based Theorem Proving",
author = "Jason J. Hickey and Aleksey Nogin",
pages = "252--266"
}
@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{NKYH05,
title = {A Computational Approach to Reflective Meta-Reasoning about Languages with Bindings},
author = {Aleksey Nogin and Alexei Kopylov and Xin Yu and Jason Hickey},
booktitle = {MERLIN '05: Proceedings of the 3rd ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding},
isbn = {1-59593-072-8},
pages = {2--12},
location = {Tallinn, Estonia},
doi = {http://doi.acm.org/10.1145/1088454.1088456},
publisher = {ACM Press},
year = 2005,
note = {An extended version is available as \href{http://resolver.caltech.edu/CaltechCSTR:2005.003}{California Institute of Technology technical report CaltechCSTR:2005.003}}
}
@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}"
}
@InProceedings{HN04,
author = {Jason Hickey and Aleksey Nogin},
title = {Extensible Hierarchical Tactic Construction in a Logical
Framework},
pages = {136--151},
crossref = {tphols2004},
url = {http://nogin.org/papers/resources.html}
}
@inproceedings{HN06a,
author = {Jason Hickey and Aleksey Nogin},
title = {{\OMake}: Designing a Scalable Build Process},
pages = {63--78},
booktitle = {Fundamental Approaches to Software Engineering, 9th
International Conference, FASE 2006},
editor = {Luciano Baresi and Reiko Heckel},
publisher = {Springer},
series = LNCS,
volume = 3922,
year = 2006,
location = {Vienna, Austria},
url = {http://dx.doi.org/10.1007/11693017_7},
note = {An extended version is available as \href{http://resolver.caltech.edu/CaltechCSTR:2006.001}{California Institute of Technology technical report CaltechCSTR:2006.001}}
}
@article{HN06b,
author = {Jason Hickey and Aleksey Nogin},
title = {Formal Compiler Construction in a Logical Framework},
journal = {Higher-Order and Symbolic Computation},
pages = {197--230},
volume = 19,
number = {2--3},
month = Sep,
year = 2006,
publisher = {Springer Netherlands},
url = {http://dx.doi.org/10.1007/s10990-006-8746-6}
}
@inproceedings{HNYK06,
author = {Jason Hickey and Aleksey Nogin and Xin Yu and Alexei Kopylov},
title = {Practical Reflection for Sequent Logics},
booktitle = {Proceedings of the International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice ({LFMTP}'06)},
series = ENTCS,
year = 2006
}
@inproceedings{HNYK06b,
author = {Jason Hickey and Aleksey Nogin and Xin Yu and Alexei Kopylov},
title = {Mechanized Meta-Reasoning Using a Hybrid {HOAS}/de {Bruijn} Representation and Reflection},
booktitle = {Proceedings of the 11th ACM SIGPLAN International Conference on Functional Programming, ICFP 2006},
publisher = {ACM},
editor = {John H. Reppy and Julia L. Lawall},
pages = {172--183},
year = 2006,
location = {Portland Oregon, USA},
url = {http://doi.acm.org/10.1145/1159803.1159826}
}
@inproceedings{NK06,
author = {Aleksey Nogin and Alexei Kopylov},
title = {Formalizing Type Operations Using the ``{Image}'' Type Constructor},
booktitle = {Proceedings of the 13th Workshop on Logic, Language, Information and Computation (WoLLIC 2006)},
series = ENTCS,
volume = 165,
pages = {121--132},
publisher = {Elsevier},
year = 2006,
url = {http://dx.doi.org/10.1016/j.entcs.2006.05.041},
}
@Techreport{Nog95,
author = "Aleksey Nogin",
title = "On {H}orn Interpolation in Linear Logic",
institution = "Steklov Mathematical Institute",
type = "Mathematical Logic and Theoretical Computer Science",
number = "TR 1995-11",
month = "April",
year = 1995,
note = "In Russian"
}
@Techreport{Nog97,
author = {Aleksey Nogin},
title = {Improving the Efficiency of {\Nuprl} Proofs},
institution = {Cornell University},
type = {Department of Computer Science},
number = {\href{http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR97-1643}{TR97-1643}},
month = {August},
year = {1997},
note = {See also \url{http://nogin.org/papers/effproof.html}}
}
@inproceedings{Nog00,
author = "Aleksey Nogin",
title = "Writing Constructive Proofs Yielding Efficient Extracted Programs",
booktitle = "Proceedings of the Workshop on Type-Theoretic Languages: Proof Search and Semantics",
volume = 37,
series = "Electronic Notes in Theoretical Computer Science",
publisher = "Elsevier Science Publishers",
editor = "Didier Galmiche",
year = 2000,
note = "\url{http://www.elsevier.nl/gej-ng/31/29/23/67/22/show/Products/notes/index.htt#005}"
}
@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{TNHW04,
Author = {Cristian Tapus and Aleksey Nogin and Jason Hickey and Jerome White},
Title = {A Simple Serializability Mechanism for a Distributed Objects System},
BookTitle = {Proceedings of the 17$^{th}$ International Conference on Parallel and Distributed Computing Systems (PDCS-2004)},
Editor = {David A. Bader and Ashfaq A. Khokhar},
ISBN = {1-880843-52-8},
Publisher = {International Society for Computers and Their Applications (ISCA)},
URL = {http://nogin.org/papers/serializability.html},
Year = 2004
}
@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{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,
}
@PROCEEDINGS{tphols2004,
KEY = {TPHOLs04},
TITLE = {Proceedings of the 17$^{th}$ International Conference on
Theorem Proving in Higher Order Logics (TPHOLs 2004)},
BOOKTITLE = {Proceedings of the 17$^{th}$ International Conference on
Theorem Proving in Higher Order Logics (TPHOLs 2004)},
SERIES = LNCS,
VOLUME = 3223,
EDITOR = {Konrad Slind and Annette Bunker and Ganesh Gopalakrishnan},
PUBLISHER = {Springer-Verlag},
YEAR = 2004,
}
@PROCEEDINGS{tphols2004b,
KEY = {TPHOLs04B},
TITLE = {Emerging Trends. Proceedings of the 17$^{th}$ International
Conference on Theorem Proving in Higher Order Logics (TPHOLs 2004)},
BOOKTITLE = {Emerging Trends. Proceedings of the 17$^{th}$ International
Conference on Theorem Proving in Higher Order Logics (TPHOLs 2004)},
EDITOR = {Konrad Slind},
PUBLISHER = {University of Utah},
YEAR = 2004,
}