Jason Hickey's Papers

I also have a page on seminars and presentations, where you can get a copy of the slides if you have seen one of my talks.

By subject

Verification and group communication protocols

Specifications and Proofs for Ensemble Layers, Jason Hickey, Nancy Lynch, and Robbert van Renesse. TACAS '99, Springer, May 1999.

An Object-Oriented Approach to Verifying Group Communication Systems, Mark Bickford and Jason Hickey, submitted to CADE-16.

Optimization of communication protocols

A Proof Environment for the Development of Group Communication Systems, Christoph Kreitz, Mark Hayden, and Jason Hickey, CADE15, LNAI 1421, 317-322, Springer 1998.

The MetaPRL Logical Framework

Fault-Tolerant Distributed Theorem Proving, Jason Hickey, submitted to CADE-16.

Fast Tactic-based Theorem Proving, Jason Hickey and Alexey Nogin, submitted to CADE-16.

Nuprl-Light: An Implementation Framework for Higher-Order Logics, Jason Hickey, CADE-14, LNAI 1249, 395-399, Springer 1997.

Modular Frameworks for Higher Order Logics, Jason Hickey.

Modules With Proofs, Jason Hickey.

Interpretations of Modules and Objects

A Predicative Type-Theoretic Interpretation of Objects, Jason Hickey.

Formal Objects in Type Theory Using Very Dependent Types, Jason Hickey. Foundations of Object-Oriented Languages 3, 1996.

Hardware optimization

Non-Restoring Integer Square Root: A Case Study in Design by Principled Optimization, John O'Leary, Miriam Leeser, Jason Hickey, Mark Aagaard. In Theorem Provers in Circuit Design - Theory Practice and Experience, Springer, 1995.

Other

Formal Abstract Data Types, Jason Hickey, note on type theory for modules.

Patent

W. S. Marcus and J. J. Hickey. Batcher and Banyan Switching Elements. U. S. Patent 5,130,976, 1992.

Bellcore papers

At Bellcore, I designed and implemented fast-packet switches for data communication. This was part of the early work on ATM. I don't have these papers online at Cornell. The listing is in chronological order.

1

C. M. Day, J. N. Giacopelli, and J. J. Hickey. Applications of Self-Routing Switches to LATA Fiber Optic Networks. In Proceedings of the International Switching Symposium, volume 3, page A7.3, Phoenix, AZ, March 1987.

2

J. N. Giacopelli, J. J. Hickey, 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):1289-1298, October 1991.

3

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

4

J. J. Hickey, T. J. Bogovic, B. S. Davie, W. S. Marcus, V. F. Massa, L. Trajkovic, and D. V. Wilson. The Architecture of the Sunshine B-ISDN Network. In Proceedings of the International Switching Symposium, Yokohama, Japan, May 1992. Submitted for Publication.

5

J. J. Hickey and W. S. Marcus. A Design for a Large, High Speed Batcher/banyan Packet Switch. Technical Report TM-ARH-014132, Bellcore, May 1989.

6

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, volume 1, pages 75-84, Stockholm, Sweden, May 1990.

 

8

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, volume 1, pages 75-84, San Francisco, CA, May 1990.