CV

by | Jan 25, 2016 | 1 comment

Jason Hickey

Member of Technical Staff
Google Inc.
1600 Amphitheatre Parkway
Mountain View, CA 94043
Citizenship: USA

Academic and Industrial Positions

2008-present Member of Technical Staff, Google Inc.  Internet of Things, Scheduling and reliability for Google’s global computing infrastructure.

2000-2008 Assistant Professor, Computer Science, California Institute of Technology.  Research interests include programming languages, formal methods, and compilers for fault-tolerant distributed systems and high-confidence control.  Developed new courses in modern operating systems, compilers, and programming language semantics.

1999-2000 Instructor, Computer Science, California Institute of Technology.

1998-1999 Programmer/Analyst, Cornell University.  Research in logical frameworks for specification and validation of large software systems.

1985-1995 Member of Technical Staff, Bellcore, Morristown NJ.  Design of fast packet switch architecture for supplanting central office switching systems, as well as high-speed ATM packet switches for the NSF-sponsored National Gigabit Testbed. Development of ATM standards, including AAL5, and ATM Forum (IP over ATM).

Education

2001 Ph.D., Cornell University, Computer Science, thesis supervisor: Robert L. Constable.
1995 M.S., Cornell University, Computer Science.
1987 M.Eng., Cornell University, Electrical Engineering.
1985 B.S. with honors, California Institute of Technology, Electrical Engineering.

Program committee membership

Logic in Computer Science (LICS)
Theorem Proving in Higher Order Logics (TPHOLs)
International Joint Conference on Automated Reasoning (IJCAR)
International Conference on Functional Programming (ICFP)
Workshop on Distributed Shared Memory (DSM)
International Conference on Control Systems and Computer Science (CSCS)
Formal Methods and Models for Codesign (MEMOCODE)
Workshop on Tools, Operating Systems and Programming Models for Developing Reliable Systems (TOPMoDelS)

Patents

John Wilkes, Todd Wang, David Oppenheimer, Brian Grant, Jason Hickey, Kai Backman, Joseph Hellerstein, David Bort, Systems and methods for performing scheduling for a cluster, 2015, U.S. Patent 9229774.

W.S. Marcus and J.J. Hickey, Batcher and Banyan Switching Elements, 1992, U.S. Patent 5130976.

Books

Yaron Minsky, Anil Madhavapeddy, Jason Hickey, Real World OCaml, 2014, O’Reilly Press, https://realworldocaml.org/.

Jason Hickey, Introduction to Objective Caml.  An older version of the book is available at http://files.metaprl.org/doc/ocaml-book.pdf.

Thesis

Jason J. Hickey, The MetaPRL Logical Programming Environment, January 2001, Ithaca, NY.

Papers

Jason Hickey and Aleksey Nogin, Formal Compiler Construction in a Logical Framework, 2005, Journal on Higher-Order and Symbolic Computation.

Constable, Robert L. and Hickey, Jason, Nuprl’s class theory and its applications, Foundations of Secure Computation, 2000, Pages 91–116, NATO ASI Series, Series F: Computer and System Sciences, IOS Press, Editors: Friedrich L. Bauer and Ralf Steinbrueggen.

Cristian Ţãpuş and Jason Hickey, Distributed Speculative Execution for Reliability and Fault Tolerance – an Operational Semantics, 2006, Springer, Submitted to Distributed Computation Journal.

Cristian Ţãpuş and Jason Hickey, A Theory of Nested Speculative Execution, 9th International Conference on Coordination Models and Languages (Coordination 2007), 2007.

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.

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.

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.  

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.

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.

Jason Hickey and Aleksey Nogin and Xin Yu and Alexei Kopylov, Mechanized Meta-Reasoning Using a Hybrid HOAS/de Bruijn Representation and Reflection, 2006, International Conference on Functional Programming (ICFP 2006). 

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), 2006, Electronic Notes in Theoretical Computer Science. 

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, 2005, Pages 2–12, ACM Press, ISBN 1-59593-072-8, An extended version is available as California Institute of Technology technical report CaltechCSTR:2005.003.

Jason Hickey and Aleksey Nogin, OMake: Designing a Scalable Build Process, Fundamental Approaches to Software Engineering (FASE06), 2006. 

Cristian Ţãpuş and Jason Hickey, Distributed Synchronization with Shared Semaphore Sets, IEEE International Symposium on Cluster Computing and the Grid (CCGRID 2005), Cardiff, UK, 2003, Workshop on Distributed Shared Memory on Clusters (DSM).

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.

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), 2004, Pages 136–151, 3223, Lecture Notes in Computer Science, Springer-Verlag, Editors: Konrad Slind and Annette Bunker and Ganesh Gopalakrishnan.

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, 2003, Pages 1–13, 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. 

 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), 2003, Pages 287–303, 2758, Lecture Notes in Computer Science, Springer-Verlag, Editors: David Basin and Burkhart Wolff. 

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, 2003, 1. 

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, 2003, Pages 319–320, Chillarege Press, Editor: Dr. Indrakshi Ray. 

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, Workshop on Distributed Shared Memory (DSM). 

Adam Granicz and Daniel Zimmerman and Jason Hickey, Rewriting UNITY, Proceedings of the 4th International Conference on Rewriting Techniques and Applications (RTA 14), June 2003, 2706, Lecture Notes in Computer Science, Springer, Editor: Eobert Nieuwenhuis. 

Granicz, Adam and Hickey, Jason, Phobos: A front-end approach to extensible compilers, 36th Hawaii International Conference on System Sciences, 2002, IEEE.

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), 2002, Pages 281–297, 2410, Lecture Notes in Computer Science, Springer-Verlag, Editors: Victor A. Carreño and Cézar A. Muñoz and Sophiène Tahar. 

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), 2000, Pages 149–161, IEEE Computer Society Press, Hilton Head, SC.

Jason J. Hickey and Aleksey Nogin, Fast Tactic-based Theorem Proving, Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000, 2000, Pages 252–266, 1869, Lecture Notes in Computer Science, Springer-Verlag, Editors: J. Harrison and M. Aagaard, http://nogin.org/papers/fast_proving.html. 

Hickey, Jason J., Fault-Tolerant Distributed Theorem Proving, Proceedings of the 16th International Conference on Automated Deduction, July 7–10 1999, Pages 227–231, 1632, Lecture Notes in Artificial Intelligence, Trento, Italy, Berlin, Editor: Harald Ganzinger, ISBN 3-540-66222-7.

Mark Bickford and Jason J. Hickey, Predicate Transformers for Infinite-State Automata in Nuprl Type Theory, Proceedings of Third Irish Workshop in Formal Methods, 1999.

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, 1999, Pages 119–133, 1579, Lecture Notes in Computer Science, Springer, Editor: W. Rance Cleaveland.

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, 1998, Pages 317–332, Lecture Notes in Artificial Intelligence, Springer. 

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), December 1999, Pages 80–92, 33(5), Operating Systems Review, ACM Press, Editors: David Kotz and John Wilkes.

Jason J. Hickey, NuPRL-Light: An Implementation Framework for Higher-Order Logics, Proceedings of the 14th International Conference on Automated Deduction, July 13–17 1997, Pages 395–399, 1249, Lecture Notes in Artificial Intelligence, 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.

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.

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, 1994, Pages 52–71, Springer-Verlag, London, UK, ISBN 3-540-59047-1.

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.

J.J. Hickey, A 50 MIP ATM Cell Processor for B-ISDN, Proceedings of the IEEE Custom Integrated Circuits Conference, May 1992.

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, October 1991, Pages 1289–1298, 9. 

J. J. Hickey and W. S. Marcus, The Implementation of a High Speed ATM Packet Switch Using CMOS VLSI, In Proceedings of the International Switching Symposium, May 1990, Pages 75–84, 1. 

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, May 1990, Pages 75–84, 1. 

J. J. Hickey and W. S. Marcus, A Design for a Large, High Speed Batcher/banyan Packet Switch, May 1989.

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, March 1987, 3.

Notes

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), 2004, Pages 57–70, University of Utah, Editor: Konrad Slind.

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.

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, 2003, Pages 13–27, Universität Freiburg, Editors: David Basin and Burkhart Wolff.

Brian Aydemir and Adam Granicz and Jason Hickey, Formal Design Environments, Theorem Proving in Higher Order Logics; Emerging Trends Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2002), Hampton, VA, August 2002, 2002, Pages 12–22, National Aeronautics and Space Administration, Editors: Victor A. Carreño and Cézar A. Muñoz and Sophiène Tahar.

Additional technical reports

Cristian Ţãpuş and Jason Hickey, Extended Operational Semantics for Simple Distributed Speculative Execution, January 2005, Caltech Computer Science.

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, July 2002, Caltech Computer Science. 

Tutorials

Jason Hickey and Aleksey Nogin and Brian Aydemir and others, Introduction to 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/.

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/.

Completed theses

Xin Yu, Reflection and its application to mechanized metareasoning about programming languages, June 2007, Department of Computer Science, Caltech, http://resolver.caltech.edu/CaltechETD:etd-05222007-211909.

Ţãpuş, Cristian, Distributed Speculations: Providing Fault-tolerance and Improving Performance, June 2006, Department of Computer Science, Caltech, http://resolver.caltech.edu/CaltechETD:etd-06022006-140421.

Ţãpuş, Cristian, Kernel Level Distributed Inter-Process Communication System (KDIPC), June 2004, Department of Computer Science, Caltech, http://resolver.caltech.edu/CaltechETD:etd-08312004-184300.

Nathaniel Asoka Gray, High-confidence, modular compiler development in a formal environment, May 2005, Department of Computer Science, Caltech. http://resolver.caltech.edu/CaltechETD:etd-12072001-160019.

Justin D. Smith, Fault Tolerance using Whole-Process Migration and Speculative Execution, 2003, Department of Computer Science, Caltech, http://resolver.caltech.edu/CaltechETD:etd-05272003-120725.

Xin Yu, Formalizing Abstract Algebra in Constructive Set Theory, June 2003, Department of Computer Science, Caltech.

Joseph Kiniry, Kind Theory, May 2002, Department of Computer Science, Caltech, http://resolver.caltech.edu/CaltechETD:etd-06062002-164914.

Roman Ginis, Automating resource management for distributed business processes, October 2001, Department of Computer Science, Caltech (co-advisor Mani Chandy), http://resolver.caltech.edu/CaltechETD:etd-11012005-093745.

Daniel Zimmerman, Dynamic UNITY, July 2001, Department of Computer Science, Caltech (co-advisor Mani Chandy), http://resolver.caltech.edu/CaltechETD:etd-12072001-160019.