Home
People
Research
Projects
Publications
Download
Laboratory
Support
CVSweb
Mailing Lists
Links
Funded by...

Papers

Distributed Systems

[crt-distrib-comp-journal06] BibTeX	Cristian Ţãpuş and Jason Hickey, Distributed Speculative Execution for Reliability and Fault Tolerance – an Operational Semantics, Distributed Computing Journal, 2006, Springer, Submitted to the Distributed Computing Journal (Springer).
[crt-spec-ppopp07] BibTeX	Cristian Ţãpuş and Jason Hickey, Speculations: Providing Fault-tolerance and Improving Performance of Parallel Applications, Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP 2007), 2007.
[crt-mcc-topmodels07] BibTeX	Justin D. Smith and Cristian Ţãpuş and Jason Hickey, The Mojave Compiler: Providing Language Primitives for Whole-Process Migration and Speculation for Distributed Applications, 2007, To be presented at the HIPS/TOPMoDelS workshop (at IPDPS 2007).
[crt-ipdps07] BibTeX	Cristian Ţãpuş and Jason Hickey, A Theory of Nested Speculative Execution, 2007, .
[crt-hotdep06] pdf BibTeX	Cristian Ţãpuş and Jason Hickey, Speculations: Providing Fault-tolerance and Recoverability in Distributed Environments, Proceedings of the Second Workshop on Hot Topics in System Dependability (HotDep '06), 2006, http://mojave.caltech.edu/crt/publications/hotdep2006.pdf.
[crt-icns06] pdf BibTeX	Cristian Ţãpuş and David Noblet and Jason Hickey, MojaveComm: A Robust Group Communication Library for Grid Environments, Proceedings of the International Conference on Networking and Services (ICNS'06), 2006, http://www.cs.caltech.edu/~crt/publications/icns2006.pdf.
[crt-ispdc06] pdf BibTeX	Cristian Ţãpuş and David Noblet and Vlad Grama and Jason Hickey, MojaveFS: Providing Sequential Consistency in a Distributed Objects System, Proceedings of the The 5th International Symposium on Parallel and Distributed Computing (ISPDC 2006), 2006, http://www.cs.caltech.edu/~crt/publications/ispdc06.pdf.
[crt-dsm05] pdf BibTeX	Cristian Ţãpuş and Jason Hickey, Distributed Synchronization with Shared Semaphore Sets, IEEE International Symposium on Cluster Computing and the Grid (CCGRID 2005), Cardiff, UK, 2005, http://www.cs.caltech.edu/~crt/publications/dsm2005.pdf, Workshop on Distributed Shared Memory on Clusters (DSM).
[TNHW04] ps pdf BibTeX	Cristian Ţãpuş and Aleksey Nogin and Jason Hickey and Jerome White, A Simple Serializability Mechanism for a Distributed Objects System, Proceedings of the 17th International Conference on Parallel and Distributed Computing Systems (PDCS-2004), 2004, International Society for Computers and Their Applications (ISCA), Editors: David A. Bader and Ashfaq A. Khokhar, ISBN 1-880843-52-8, http://nogin.org/papers/serializability.html.
[crt-dsm03] pdf BibTeX	Cristian Ţãpuş and Justin D. Smith and Jason Hickey, Kernel Level Speculative DSM, IEEE International Symposium on Cluster Computing and the Grid (CCGRID 2003), Tokyo, Japan, 2003, http://www.cs.caltech.edu/~crt/publications/dsm2003.pdf, Workshop on Distributed Shared Memory (DSM).
[BCHH00] link BibTeX	Ken Birman and Robert Constable and Mark Hayden and Jason Hickey and Christoph Kreitz and Robbert van Renesse and Ohad Rodeh and Werner Vogels, The Horus and Ensemble Projects: Accomplishments and Limitations., DARPA Information Survivability Conference and Exposition (DISCEX 2000), Pages 149–161, 2000, IEEE Computer Society Press, Hilton Head, SC.

Programming languages and compilers

[HNYK06b] link pdf BibTeX	Jason Hickey and Aleksey Nogin and Xin Yu and Alexei Kopylov, Mechanized Meta-Reasoning Using a Hybrid HOAS/de Bruijn Representation and Reflection, Proceedings of the 11th ACM SIGPLAN International Conference on Functional Programming, ICFP 2006, Pages 172–183, 2006, ACM, Editors: John H. Reppy and Julia L. Lawall, http://nogin.org/papers/reflection2.html.
[HNYK06] pdf BibTeX	Jason Hickey and Aleksey Nogin and Xin Yu and Alexei Kopylov, Practical Reflection for Sequent Logics, Proceedings of the International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'06), Electronic Notes in Theoretical Computer Science, 2006, http://nogin.org/papers/reflection3.html.
[HN06] link BibTeX	Jason Hickey and Aleksey Nogin, Formal Compiler Construction in a Logical Framework, Higher-Order and Symbolic Computation, 19, (2–3), Pages 197–230, September 2006, Springer Netherlands, http://dx.doi.org/10.1007/s10990-006-8746-6.
[NKYH05] link TR link BibTeX	Aleksey Nogin and Alexei Kopylov and Xin Yu and Jason Hickey, A Computational Approach to Reflective Meta-Reasoning about Languages with Bindings, MERLIN '05: Proceedings of the 3rd ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding, Pages 2–12, 2005, ACM Press, ISBN 1-59593-072-8, An extended version is available as California Institute of Technology technical report CaltechCSTR:2005.003.
[GHNT04] pdf BibTeX	Nathaniel Gray and Jason Hickey and Aleksey Nogin and Cristian Ţãpuş , Building Extensible Compilers in a Formal Framework. A Formal Framework User's Perspective, Emerging Trends. Proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2004), Pages 57–70, 2004, University of Utah, Editor: Konrad Slind, http://nogin.org/papers/mmc-tphols.html.
[HNGA03] link TR link BibTeX	Jason Hickey and Aleksey Nogin and Adam Granicz and Brian Aydemir, Compiler implementation in a formal logical framework, Proceedings of the 2003 workshop on Mechanized reasoning about languages with variable binding, Pages 1–13, 2003, ACM Press, ISBN 1-58113-800-8/03/0008, http://doi.acm.org/10.1145/976571.976575, An extended version of the paper is available as Caltech Technical Report caltechCSTR:2003.002.
[GTNH03] pdf BibTeX	Nathaniel Gray and Cristian Ţãpuş and Aleksey Nogin and Jason Hickey, Building Reliable Compilers with a Formal Methods Framework, The 14th International Symposium on Software Reliability Engineering (ISSRE 2003). Supplementary Proceedings, Pages 319–320, 2003, Chillarege Press, Editor: Dr. Indrakshi Ray, http://nogin.org/papers/mojavec.html.
[GH02] ps pdf TR ps BibTeX	Granicz, Adam and Hickey, Jason, Phobos: A front-end approach to extensible compilers, 36th Hawaii International Conference on System Sciences, 2002, IEEE.
[AGH02] ps BibTeX	Brian Aydemir and Adam Granicz and Jason Hickey, Formal Design Environments, Theorem Proving in Higher Order Logics; Track B Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2002), Hampton, VA, August 2002, Pages 12–22, 2002, National Aeronautics and Space Administration, Editors: Victor A. Carreño and Cézar A. Muñoz and Sophiène Tahar.

OMake

[HN05c]
link ps pdf TR ps TR pdf TR link BibTeX

Jason Hickey and Aleksey Nogin, OMake: Designing a Scalable Build Process, Fundamental Approaches to Software Engineering, 9th International Conference, FASE 2006, Lecture Notes in Computer Science, 3922, Pages 63–78, 2006, Springer, Editors: Luciano Baresi and Reiko Heckel, http://nogin.org/papers/omake.html, An extended version is available as California Institute of Technology technical report CaltechCSTR:2006.001.

The MetaPRL logical framework

[NK06] link pdf BibTeX	Aleksey Nogin and Alexei Kopylov, Formalizing Type Operations Using the ``Image'' Type Constructor, Proceedings of the 13th Workshop on Logic, Language, Information and Computation (WoLLIC 2006), Electronic Notes in Theoretical Computer Science, 165, Pages 121–132, 2006, Elsevier, http://dx.doi.org/10.1016/j.entcs.2006.05.041.
[HN04] link BibTeX	Jason Hickey and Aleksey Nogin, Extensible Hierarchical Tactic Construction in a Logical Framework, Proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2004), Lecture Notes in Computer Science, 3223, Pages 136–151, 2004, Springer-Verlag, Editors: Konrad Slind and Annette Bunker and Ganesh Gopalakrishnan, http://nogin.org/papers/resources.html.
[HNC+03] link BibTeX	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, MetaPRL — A Modular Logical Environment, Proceedings of the 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2003), Lecture Notes in Computer Science, 2758, Pages 287–303, 2003, Springer-Verlag, Editors: David Basin and Burkhart Wolff, http://nogin.org/papers/metaprl.html.
[BKKN03] link BibTeX	Yegor Bryukhov and Alexei Kopylov and Vladimir Krupski and Aleksey Nogin, Implementing and Automating Basic Number Theory in MetaPRL Proof Assistant, 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2003). Emerging Trends Proceedings, Pages 29–39, 2003, Universität Freiburg, Editors: David Basin and Burkhart Wolff, http://nogin.org/papers/arith.html.
[CABCHK03] pdf BibTeX	Constable, Robert L. and Stuart Allen and Mark Bickford and James Caldwell and Jason Hickey and Christoph Kreitz, Steps Toward a World Wide Digital Library of Formal Algorithmic Knowledge, 1, 2003, http://www.nuprl.org/FDLproject/muriOct28_web.pdf, MURI Review.
[Nog02b] link TR pdf BibTeX	Aleksey Nogin, Quotient Types: A Modular Approach, Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2002), Lecture Notes in Computer Science, 2410, Pages 263–280, 2002, Springer-Verlag, Editors: Victor A. Carreño and Cézar A. Muñoz and Sophiène Tahar, ISBN 3-540-44039-9, http://nogin.org/papers/quotients.html.
[Nog02c] link BibTeX	Aleksey Nogin, Theory and Implementation of an Efficient Tactic-Based Logical Framework, August 2002, Ithaca, NY, http://nogin.org/papers/thesis.html.
[NH02] link BibTeX	Aleksey Nogin and Jason Hickey, Sequent Schema for Derived Rules, Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2002), Lecture Notes in Computer Science, 2410, Pages 281–297, 2002, Springer-Verlag, Editors: Victor A. Carreño and Cézar A. Muñoz and Sophiène Tahar, ISBN 3-540-44039-9, http://nogin.org/papers/derived_rules.html.
[KN01] link BibTeX	Alexei Kopylov and Aleksey Nogin, Markov's Principle for Propositional Type Theory, Computer Science Logic, Proceedings of the 10th Annual Conference of the EACSL, Lecture Notes in Computer Science, 2142, Pages 570–584, 2001, Springer-Verlag, Editor: L. Fribourg, http://nogin.org/papers/markov.html.
[SLKN01] link BibTeX	Stephan Schmitt and Lori Lorigo and Christoph Kreitz and Aleksey Nogin, JProver: Integrating Connection-Based Theorem Proving into Interactive Proof Assistants, International Joint Conference on Automated Reasoning, Lecture Notes in Artificial Intelligence, 2083, Pages 421–426, 2001, Springer-Verlag, http://nogin.org/papers/jprover.html.
[HN00] link BibTeX	Jason J. Hickey and Aleksey Nogin, Fast Tactic-based Theorem Proving, Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000, Lecture Notes in Computer Science, 1869, Pages 252–266, 2000, Springer-Verlag, Editors: J. Harrison and M. Aagaard, http://nogin.org/papers/fast_proving.html.
[Nog00] link BibTeX	Aleksey Nogin, Writing Constructive Proofs Yielding Efficient Extracted Programs, Proceedings of the Workshop on Type-Theoretic Languages: Proof Search and Semantics, Electronic Notes in Theoretical Computer Science, 37, 2000, Elsevier Science Publishers, Editor: Didier Galmiche, http://www.elsevier.nl/gej-ng/31/29/23/67/22/show/Products/notes/index.htt#005.
[Hic99b] ps pdf BibTeX	Hickey, Jason J., Fault-Tolerant Distributed Theorem Proving, Proceedings of the 16th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, 1632, Pages 227–231, July 7–10 1999, Trento, Italy, Berlin, Editor: Harald Ganzinger, ISBN 3-540-66222-7.
[Hic97b] link ps pdf BibTeX	Jason J. Hickey, NuPRL-Light: An Implementation Framework for Higher-Order Logics, Proceedings of the 14th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, 1249, Pages 395–399, July 13–17 1997, Springer, Editor: William McCune, ISBN 3-540-63104-6, An extended version of the paper can be found at http://www.cs.caltech.edu/~jyh/papers/cade14_nl/default.html.

Formal methods

[GZH03] ps pdf BibTeX	Adam Granicz and Daniel Zimmerman and Jason Hickey, Rewriting UNITY, Proceedings of the 4th International Conference on Rewriting Techniques and Applications (RTA 14), Lecture Notes in Computer Science, 2706, June 2003, Springer, Editor: Eobert Nieuwenhuis.
[YNKH03] link BibTeX	Xin Yu and Aleksey Nogin and Alexei Kopylov and Jason Hickey, Formalizing Abstract Algebra in Type Theory with Dependent Records, 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2003). Emerging Trends Proceedings, Pages 13–27, 2003, Universität Freiburg, Editors: David Basin and Burkhart Wolff, http://nogin.org/papers/formalaa.html.
[CH00] link BibTeX	Constable, Robert L. and Hickey, Jason, Nuprl's class theory and its applications, Foundations of Secure Computation, NATO ASI Series, Series F: Computer \& System Sciences, Pages 91–116, 2000, IOS Press, Editors: Friedrich L. Bauer and Ralf Steinbrueggen.
[KHH98] ps pdf BibTeX	Kreitz, Christoph and Mark Hayden and Jason J. Hickey, A Proof Environment for the Development of Group Communications Systems, Fifteen International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, 1421, Pages 317–332, 1998, Springer.
[BH99] pdf BibTeX	Mark Bickford and Jason J. Hickey, Predicate Transformers for Infinite-State Automata in Nuprl Type Theory, Proceedings of 3^rd Irish Workshop in Formal Methods, 1999.
[HLV99] ps pdf BibTeX	Jason J. Hickey and Nancy Lynch and Robbert van Renesse, Specifications and Proofs for Ensemble Layers, 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, 1579, Pages 119–133, 1999, Springer, Editor: W. Rance Cleaveland, http://link.springer-ny.com/link/service/series/0558/tocs/t1579.htm.

Theses

[crt-phd-thesis] pdf BibTeX	Ţãpuş, Cristian, Distributed Speculations: Providing Fault-tolerance and Improving Performance, June 2006, Pasadena, CA, http://etd.caltech.edu/etd/available/etd-06022006-140421/.
[crt-ms-thesis] pdf BibTeX	Ţãpuş, Cristian, Kernel Level Distributed Inter-Process Communication System (KDIPC), June 2004, Pasadena, CA, http://etd.caltech.edu/etd/available/etd-08312004-184300/.
[Gra05] link BibTeX	Nathaniel Asoka Gray, High-confidence, modular compiler development in a formal environment, May 2005, Department of Computer Science.
[Smi03] link BibTeX	Justin D. Smith, Fault Tolerance using Whole-Process Migration and Speculative Execution, 2003, Department of Computer Science.
[YH03] pdf BibTeX	Xin Yu and Jason J. Hickey, Formalizing Abstract Algebra in Constructive Set Theory, CSTR2003.004, June 2003, Pasadena, CA, http://caltechcstr.library.caltech.edu/secure/00000491/01/formalaa.pdf.
[Kin02] link BibTeX	Joseph Kiniry, Kind Theory, May 2002, Department of Computer Science.
[Gin01b] link BibTeX	Roman Ginis, Automating resource management for distributed business processes, October 2001, Department of Computer Science (co-advised with Mani Chandy).
[Zim01] link BibTeX	Daniel Zimmerman, Dynamic UNITY, July 2001, Department of Computer Science (co-advised with Mani Chandy).

Technical Reports

[crt-tech-report1] TR link BibTeX	Jason Hickey and Justin D. Smith and Brian Aydemir and Nathaniel Gray and Adam Granicz and Cristian Ţãpuş, Process Migration and Transactions Using a Novel Intermediate Language, caltechCSTR 2002.007, July 2002, Computer Science.
[crt-tech-report2] TR link BibTeX	Cristian Ţãpuş and Jason Hickey, Extended Operational Semantics for Simple Distributed Speculative Execution, caltechCSTR 2005.002, January 2005, Computer Science.
[HNGA03] link TR link BibTeX	Jason Hickey and Aleksey Nogin and Adam Granicz and Brian Aydemir, Compiler implementation in a formal logical framework, Proceedings of the 2003 workshop on Mechanized reasoning about languages with variable binding, Pages 1–13, 2003, ACM Press, ISBN 1-58113-800-8/03/0008, http://doi.acm.org/10.1145/976571.976575, An extended version of the paper is available as Caltech Technical Report caltechCSTR:2003.002.

Workshops and courses

[HNA+04] BibTeX	Jason Hickey and Aleksey Nogin and Brian Aydemir and others, Introduction into formal computer-aided reasoning and the MetaPRL theorem prover, June 2004, Tutorial given at the North American Summer School in Logic, Language and Information (NASSLI 2004), http://tutorial.metaprl.org/.
[HNA+03] BibTeX	Jason Hickey and Aleksey Nogin and Brian Aydemir and others, Introduction to MetaPRL Theorem Prover, September 2003, Tutorial given at TPHOLs 2003, Rome, Italy, http://tutorial.metaprl.org/.

MetaPRL Online Publications

[MojaveHome] link BibTeX	Jason J. Hickey and others, Mojave Research Project Home Page, http://mojave.caltech.edu/.
[MPHome] link BibTeX	Jason J. Hickey and Aleksey Nogin and Alexei Kopylov and others, MetaPRL Home Page, http://metaprl.org/.
[MPthe] link BibTeX	Jason J. Hickey and Brian Aydemir and Yegor Bryukhov and Alexei Kopylov and Aleksey Nogin and Xin Yu, A Listing of MetaPRL Theories, http://metaprl.org/theories.pdf.
[OMakeHome] link BibTeX	Jason J. Hickey and Aleksey Nogin and others, The OMake Home Page, http://omake.metaprl.org/.
[MetaprlUserGuide] link BibTeX	Jason Hickey and Aleksey Nogin and Alexei Kopylov, The MetaPRL User Guide, http://metaprl.org/user-guide/default.html.
[MetaprlDeveloperGuide] link BibTeX	Aleksey Nogin and Vladimir Krupski, The MetaPRL Developer Guide, http://metaprl.org/developer-guide/default.html.

Webmaster | Contact Us | Generated on Sat Jan 27 19:01:31 PST 2007

Copyright (c) 2002-2006 Caltech Mojave Research Group.
Computer Science Department, California Institute of Technology