Publications
| [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, HIPS/TOPMoDelS workshop (at IPDPS 2007), 2007. |
| [crt-ipdps07] BibTeX |
Cristian Ţãpuş and Jason Hickey, A Theory of Nested Speculative Execution, 9th International Conference on Coordination Models and Languages (Coordination 2007), 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. |
| [HNYK06b] link pdfBibTeX |
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. |
| [HN05a] 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. |
| [HN05c] link ps pdfTR ps TR pdfTR linkBibTeX |
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. |
| [NKYH05] link TR linkBibTeX |
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, http://doi.acm.org/10.1145/1088454.1088456, An extended version is available as California Institute of Technology technical report CaltechCSTR:2005.003. |
| [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). |
| [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. |
| [TNHW04] ps pdfBibTeX |
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. |
| [HN04] link BibTeX |
Jason Hickey and Aleksey Nogin, Extensible Hierarchical Tactic Construction in a Logical Framework, Proceedings of the 17thInternational 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. |
| [YH04] BibTeX |
Xin Yu and Jason J. Hickey, The Axiomatization of Group Theory: An Experiment in Constructive Set Theory, Emerging Trends. Proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2004), 2004, University of Utah, Editor: Konrad Slind. |
| [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. |
| [HNGA03] link TR linkBibTeX |
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. |
| [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). |
| [GZH03] ps pdfBibTeX |
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. |
| [GH02] ps pdf TR psBibTeX |
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. |
| [Nog02b] link TR pdfBibTeX |
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 10thAnnual 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. |
| [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. |
| [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. |
| [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. |
| [Hic99b] ps pdfBibTeX |
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. |
| [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 pdfBibTeX |
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. |
| [KHH98] ps pdfBibTeX |
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. |
| [SOSP99] link BibTeX |
Xiaoming Liu and Christoph Kreitz and Robbert van Renesse and Jason J. Hickey and Mark Hayden and Kenneth Birman and Robert Constable, Building Reliable, High-Performance Communication Systems from Components, 17th ACM Symposium on Operating Systems Principles (SOSP’99), Operating Systems Review, 33(5), Pages 80–92, December 1999, ACM Press, Editors: David Kotz and John Wilkes. |
| [Hic97b] link ps pdfBibTeX |
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 athttp://www.cs.caltech.edu/~jyh/papers/cade14_nl/default.html. |
| [Hic96a] ps pdfBibTeX |
Jason J. Hickey, Formal Objects in Type Theory Using Very Dependent Types, Foundations of Object Oriented Languages 3, 1996, Available electronically through the FOOL 3 home page. |
| [LLHA94] link pdfBibTeX |
John W. O’Leary and Miriam Leeser and Jason Hickey and Mark Aagaard, Non-Restoring Integer Square Root: A Case Study in Design by Principled Optimization, TPCD ’94: Proceedings of the Second International Conference on Theorem Provers in Circuit Design – Theory, Practice and Experience, Pages 52–71, 1994, Springer-Verlag, London, UK, ISBN 3-540-59047-1. |
| [HBD+92] BibTeX |
J. J. Hickey and T. J. Bogovic and B. S. Davie and W. S. Marcus and V. F. Massa and L. Trajkovic and D. V. Wilson, The Architecture of the Sunshine B-ISDN Network, Proceedings of the International Switching Symposium, May 1992. |
| [Hic92] BibTeX |
J.J. Hickey, A 50 MIP ATM Cell Processor for B-ISDN, Proceedings of the IEEE Custom Integrated Circuits Conference, May 1992. |
| [GHMS91] BibTeX |
J. N. Giacopelli and J. J. Hickey and W. S. Marcus and W. D. Sincoskie, Sunshine: a High Performance Self-Routing Broadband Packet Switch Architecture, IEEE Journal on Selected Areas in Communications, 9, (8), Pages 1289–1298, October 1991. |
| [HM90] BibTeX |
Joseph Y. Halpern and Yoram Moses, Knowledge and Common Knowledge in a Distributed Environment, Journal of the Association for Computing Machinery, 37, (3), Pages 549–587, 1990. |
| [MH90] BibTeX |
W. S. Marcus and J. J. Hickey, A CMOS Batcher and Banyan Chip Set for B-ISDN, In Proceedings of IEEE International Solid State Circuits Conference, 1, Pages 75–84, May 1990. |
| [HM89] BibTeX |
J. J. Hickey and W. S. Marcus, A Design for a Large, High Speed Batcher/banyan Packet Switch, TM-ARH-014132, May 1989. |
| [DGH87] BibTeX |
C. M. Day and J. N. Giacopelli and J. J. Hickey, Applications of Self-Routing Switches to LATA Fiber Optic Networks, Proceedings of the International Switching Symposium, 3, March 1987. |
Technical Reports
| [crt-tech-report1] TR linkBibTeX |
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 linkBibTeX |
Cristian Ţãpuş and Jason Hickey, Extended Operational Semantics for Simple Distributed Speculative Execution, caltechCSTR 2005.002, January 2005, Computer Science. |
| [HSA+02] TR linkBibTeX |
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. |
| [HNGA03] link TR linkBibTeX |
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. |
| [fir-tr1] TR linkBibTeX |
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, August 2002, Computer Science. |
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/. |
Thesis
| [Hic01] link BibTeX |
Jason J. Hickey, The MetaPRL Logical Programming Environment, January 2001, Ithaca, NY,http://www.nuprl.org/documents/Hickey/Hickeythesis.html. |
Patents
| [MH92] BibTeX |
W.S. Marcus and J.J. Hickey, Batcher and Banyan Switching Elements, 1992, U.S. Patent 5130976. |
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: |