Allen, S.F.: A non-type-theoretic definition of martin-löfs types. In: LICS, pp. 215-221. IEEE Computer Society (1987)
Allen, S.F.: A Non-Type-Theoretic Semantics for Type-Theoretic Language. PhD thesis, Cornell University (1987)
Allen, S.F., Bickford, M., Constable, R.L., Eaton, R., Kreitz, C., Lorigo, L., Moran, E.: Innovations in computational type theory using Nuprl. J. Applied Logic 4(4), 428-469 (2006)
Barzilay, E.: Implementing Reflection in Nuprl. PhD thesis, Cornell University (2006)
Berghofer, S.: Program extraction in simply-typed higher order logic. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol. 2646, pp. 21-38. Springer, Heidelberg (2003)
Berghofer, S., Nipkow, T.: Executing higher order logic. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES 2000. LNCS, vol. 2277, pp. 24-40. Springer, Heidelberg (2002)
Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development. Springer (2004)
Bickford, M.: Component specification using event classes. In: Lewis, G.A., Poernomo, I., Hofmeister, C. (eds.) CBSE 2009. LNCS, vol. 5582, pp. 140-155. Springer, Heidelberg (2009)
Bickford, M., Constable, R., Guaspari, D.: Generating event logics with higherorder processes as realizers. Technical report, Cornell University (2010)
Bickford, M., Constable, R.L.: Formal foundations of computer security. In: NATO Science for Peace and Security Series, D: Information and Communication Security, vol. 14, pp. 29-52 (2008)
Bickford, M., Constable, R.L., Rahli, V.: Logic of events, a framework to reason about distributed systems. In: Languages for Distributed Algorithms Workshop (2012)
Charron-Bost, B., Schiper, A.: The Heard-Of model: Computing in distributed systems with benign failures. Distributed Computing 22(1), 49-71 (2009)
Chlipala, A.: A verified compiler for an impure functional language. In: 37th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, pp. 93-106. ACM (2010)
Constable, R.L., Allen, S.F., Bromley, H.M., Cleaveland, W.R., Cremer, J.F., Harper, R.W., Howe, D.J., Knoblock, T.B., Mendler, N.P., Panangaden, P., Sasaki, J.T., Smith, S.F.: Implementing mathematics with the Nuprl proof development system. Prentice-Hall, Inc., Upper Saddle River (1986)
Constable, R.L., Smith, S.F.: Computational foundations of basic recursive function theory. Theoretical Computer Science 121(1&2), 89-112 (1993)
Crary, K.: Type-Theoretic Methodology for Practical Programming Languages. PhD thesis, Cornell University, Ithaca, NY (August 1998)
Gordon, A.D.: Bisimilarity as a theory of functional programming. Electr. Notes Theor. Comput. Sci. 1, 232-252 (1995)
Hickey, J., et al.: MetaPRL - A modular logical environment. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 287-303. Springer, Heidelberg (2003)
Hickey, J.J.: The MetaPRL Logical Programming Environment. PhD thesis, Cornell University, Ithaca, NY (January 2001)
Howe, D.J.: Equality in lazy computation systems. In: Proceedings of Fourth IEEE Symposium on Logic in Computer Science, pp. 198-203. IEEE Computer Society (1989)
Howe, D.J.: Proving congruence of bisimulation in functional programming languages. Inf. Comput. 124(2), 103-112 (1996)
Kopylov, A.: Dependent intersection: A new way of defining records in type theory. In: LICS, pp. 86-95. IEEE Computer Society (2003)
Kopylov, A.: Type Theoretical Foundations for Data Structures, Classes, and Objects. PhD thesis, Cornell University, Ithaca, NY (2004)
Kreitz, C.: The Nuprl Proof Development System, Version 5, Reference Manual and Users Guide. Cornell University, Ithaca, NY (2002), http://www.nuprl.org/html/02cucs-NuprlManual.pdf
Leroy, X.: Formal certification of a compiler back-end or: Programming a compiler with a proof assistant. In: 33rd ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, pp. 42-54. ACM (2006)
Li, G.: Formal Verification of Programs and Their Transformations. PhD thesis, University of Utah (2010)
McCarthy, J.: Recursive functions of symbolic expressions and their computation by machine, Part I. Commun. ACM 3(4), 184-195 (1960)
Mendler, P.F.: Inductive Definition in Type Theory. PhD thesis, Cornell University, Ithaca, NY (1988)
Rahli, V., Schiper, N., Renesse, R.V., Bickford, M., Constable, R.L.: A diversified and correct-by-construction broadcast service. In: The 2nd Intl Workshop on Rigorous Protocol Engineering (WRiPE), Austin, TX (October 2012)
Schiper, N., Rahli, V., Van Renesse, R., Bickford, M., Constable, R.L.: ShadowDB: A replicated database on a synthesized consensus core. In: Eighth Workshop on Hot Topics in System Dependability, HotDep 2012 (2012)
Smith, S.F.: Partial Objects in Type Theory. PhD thesis, Cornell University, Ithaca, NY (1989)
