Skip to main content
PRL Project

References

[ABC+06]    Stuart F. Allen, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo, and E. Moran. Innovations in computational type theory using nuprl. J. Applied Logic, 4(4):428–469, 2006.

[BC08]    Mark Bickford and Robert L. Constable. Formal foundations of computer security. In NATO Science for Peace and Security Series, D: Information and Communication Security, volume 14, pages 29–52. 2008.

[BCG10]    Mark Bickford, Robert Constable, and David Guaspari. Generating event logics with higher-order processes as realizers. Technical report, Cornell University, 2010.

[BCH+00]    Ken Birman, Robert Constable, Mark Hayden, Jason Hickey, Christoph Kreitz, Robbert van Renesse, Ohad Rodeh, and Werner Vogels. The Horus and Ensemble projects: Accomplishments and limitations. In In DARPA Information Survivability Conference and Exposition (DISCEX 2000), pages 149–160. IEEE Computer Society Press, 2000.

[Bic09]    Mark Bickford. Component specification using event classes. In Component-Based Software Engineering, 12th Int’l Symp., volume 5582 of LNCS, pages 140–155. Springer, 2009.

[BKR01]    Mark Bickford, Christoph Kreitz, and Robbert Van Renesse. Formally verifying hybrid protocols with the nuprl logical programming environment. Technical report, Cornell University, 2001.

[CAB+86]    R. L. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, D. J. Howe, T. B. Knoblock, N. P. Mendler, P. Panangaden, J. T. Sasaki, and S. F. Smith. Implementing mathematics with the Nuprl proof development system. Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1986.

[CHP84]    Guy Cousineau, Gérard Huet, and Larry Paulson. The ML handbook, 1984.

[FLP85]    Michael J. Fischer, Nancy A. Lynch, and Mike Paterson. Impossibility of distributed consensus with one faulty process. J. ACM, 32(2):374–382, 1985.

[GMW79]    Michael J. C. Gordon, Robin Milner, and Christopher P. Wadsworth. Edinburgh LCF: A Mechanised Logic of Computation., volume 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979.

[Hay98]    Mark Hayden. The Ensemble System. PhD thesis, Cornell University, Department of Computer Science, 1998. Technical Report TR98-1662.

[KHH98]    Christoph Kreitz, Mark Hayden, and Jason Hickey. A proof environment for the development of group communication systems. In Automated Deduction - CADE-15, 15th Int’l Conf. on Automated Deduction, volume 1421 of Lecture Notes in Computer Science, pages 317–332. Springer, 1998.

[KR11]    Christoph Kreitz and Vincent Rahli. Introduction to Classic ML, 2011.

[Kre02]    Christoph Kreitz. The Nuprl Proof Development System, Version 5, Reference Manual and User’s Guide. Cornell University, Ithaca, NY, 2002. http://www.nuprl.org/html/02cucs-NuprlManual.pdf.

[Lam78]    Leslie Lamport. Time, clocks, and the ordering of events in a distributed system. Commun. ACM, 21(7):558–565, 1978.

[Ler00]    Xavier Leroy. The Objective Caml system release 3.00. Institut National de Recherche en Informatique et en Automatique, 2000.

[LKvR+99]   Xiaoming Liu, Christoph Kreitz, Robbert van Renesse, Jason Hickey, Mark Hayden, Kenneth P. Birman, and Robert L. Constable. Building reliable, high-performance communication systems from components. In SOSP, pages 80–92, 1999.

[Ren11]    Robbert Van Renesse. Paxos made moderately complex. www.cs.cornell.edu/courses/CS7412/2011sp/paxos.pdf, 2011.

[Win88]    Glynn Winskel. An introduction to event structures. In Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, School/Workshop, volume 354 of LNCS, pages 364–397. Springer, 1988.