Innovations in computational type theory using Nuprl

Aagaard, 1993, Verifying a logic synthesis tool in Nuprl, vol. 663, 72 Abbott, 1998, Openmath: Communicating mathematical information between co-operating agents in a knowledge network, J. Intelligent Syst., 10.1515/JISYS.1998.8.3-4.401 Allen, 2000, The Nuprl open logical environment, vol. 1831, 170 S. Allen, M. Bickford, R. Constable, R. Eaton, C. Kreitz, A Nuprl-PVS connection: Integrating libraries of formal mathematics, Technical Report, Cornell University. Department of Computer Science, 2003 S.F. Allen, A non-type-theoretic definition of Martin-Löf's types, in: [51], pp. 215–224 S.F. Allen, A non-type-theoretic semantics for type-theoretic language, PhD thesis, Cornell University, 1987 S.F. Allen, From dy/dx to [ ]p: a matter of notation, in: Proceedings of the Conference on User Interfaces for Theorem Provers, Eindhoven, The Netherlands, 1998 Allen, 2004, Abstract identifiers, intertextual reference and a computational basis for recordkeeping, First Monday, 9, 10.5210/fm.v9i2.1119 Asperti, 2003, Mathematical knowledge management in HELM, Ann. Math. Artificial Intelligence, 38, 27, 10.1023/A:1022907629104 Backhouse, 1988, Do-it-yourself type theory (part II), EATCS Bull., 35, 205 A.L. Barabsi, R. Albert, Emergence of scaling in random networks, pp. 509–512 Barendregt, 1992 J.L. Bates, A logic for correct program development, PhD thesis, Cornell University, 1979 Bates, 1985, Proofs as programs, ACM Trans. Programming Lang. Syst., 7, 53, 10.1145/2363.2528 Bertot, 2004, Interactive Theorem Proving and Program Development; Coq'Art: The Calculus of Inductive Constructions Betarte, 1998, Extension of Martin-Löf's type theory with record types and subtyping, 21 M. Bickford, R.L. Constable, A logic of events, Technical Report TR2003-1893, Cornell University, 2003 Bickford, 2001, Proving hybrid protocols correct, vol. 2152, 105 Birman, 2000, The Horus and Ensemble projects: Accomplishments and limitations, 149 Bishop, 1967 Bourbaki, 1968 Boyer, 1979 Carlisle Church, 1956 Constable, 1971, Constructive mathematics and automatic program writers, 229 Constable, 1983, Mathematics as programming, vol. 164, 116 R.L. Constable, The semantics of evidence, Technical Report TR85-684, Cornell University, 1985 Constable, 1996, Creating and evaluating interactive formal courseware for mathematics and computing Constable, 1998, Types in logic, mathematics and programming, 683 R.L. Constable, S. Allen, M. Bickford, J. Caldwell, J. Hickey, C. Kreitz, Steps Toward a World Wide Digital Library of Formal Algorithmic Knowledge, vol. 1, 2003 Constable, 1986 Constable, 2000, Nuprl's class theory and its applications, 91 Constable, 1990, Implementing metamathematics as an approach to automatic theorem proving, 45 Constable, 2000, Constructively formalizing automata, 213 Constable, 1982, Introduction to the PL/CV2 Programming Logic, vol. 135 Constable, 1979, A PL/CV précis, 7 Constable, 1984, Writing programs that construct proofs, J. Automat. Reason., 1, 285 Constable, 1978 Constable, 1984, The type theory of PL/CV3, ACM Trans. Programming Languages and Systems, 6, 94, 10.1145/357233.357238 C. Cornes, J. Courant, J.-C. Filliâtre, G. Huet, P. Manoury, C. Paulin-Mohring, C. Muñoz, C. Murthy, C. Parent, A. Saïbi, B. Werner, The Coq Proof Assistant reference manual, Technical Report, INRIA, 1995 K. Crary, Foundations for the implementation of higher-order subtyping, in: 1997 ACM SIGPLAN International Conference on Functional Programming, 1997 K. Crary, Simple, efficient object encoding using intersection types, Technical Report TR98-1675, Department of Computer Science, Cornell University, April 1998 K. Crary, Type-theoretic methodology for practical programming languages, PhD thesis, Cornell University, Ithaca, NY, August 1998 Curry, 1958, Combinatory Logic, vol. I de Bruijn, 1970, The mathematical language Automath: its usage and some of its extensions, vol. 125, 29 Dybjer, 1991, Inductive sets and families in Martin-Löf's type theory and their set-theoretic semantics, 280 A. Felty, F. Stomp, A correctness proof of a cache coherence protocol, in: Proceedings of 11th Annual Conference on Computer Assurance, 1996, pp. 128–141 Felty, 1997, Hybrid interactive theorem proving using Nuprl and HOL, vol. 1249, 351 Girard, 1989, Proofs and Types, vol. 7 Gordon, 1979, Edinburgh LCF: A Mechanized Logic of Computation, vol. 78 1987 T.G. Griffin, Notational definition and top-down refinement for interactive proof development systems, PhD thesis, Cornell University, 1988 R. Harper, M. Lillibridge, A type-theoretic approach to higher-order modules with sharing, in: Proceedings of 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, OR, January 1994, pp. 123–137 Harper, 1993, On the type structure of standard ML, ACM Trans. Programming Lang. Syst., 15, 211, 10.1145/169701.169696 HELM Hickey, 1999, Specifications and proofs for Ensemble layers, vol. 1579, 119 Hickey, 2003, MetaPRL—A modular logical environment, vol. 2758, 287 J.J. Hickey, The MetaPRL logical programming environment, PhD thesis, Cornell University, January 2001 Hoare, 1972, Notes on data structuring J.G. Hook, D.J. Howe, Impredicative strong existential equivalent to type:type, Technical Report TR 86-760, Cornell University, Department of Computer Science, June 1986 Howard, 1980, The formulas-as-types notion of construction, 479 Howe, 1987, The computational behaviour of Girard's paradox, 205 D.J. Howe, Equality in lazy computation systems, in: Proceedings of 4th IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, pp. 198–203 Howe, 1996, Importing mathematics from HOL into Nuprl, vol. 1125, 267 Howe, 1996, Semantic foundations for embedding HOL in Nuprl, vol. 1101, 85 Howe Howe, 2000, Toward sharing libraries of mathematics between theorem provers, vol. 7, 161 Jackson, 1994, Exploring abstract algebra in constructive type theory, vol. 814 Kleene, 1952 J. Kleinberg, Authoritative sources in a hyperlinked environment, Proceedings of the Ninth ACM-SIAM Symposium on Discrete Algorithms, 1998 T. Knoblock, Metamathematical extensibility in type theory, PhD thesis, Cornell University, 1987 M. Kohlhase, OmDoc: An infrastructure for openmath content dictionary information, in: Bulletin of the ACM Special Interest Group for Algorithmic Mathematics SIGSAM, 2000 Kohlhase, 2000, OmDoc: Towards an Internet standard for the administration, distribution and teaching of mathematical knowledge, vol. 1930 A. Kopylov, Dependent intersection: A new way of defining records in type theory, Department of Computer Science TR2000-1809, Cornell University, 2000 A. Kopylov, Dependent intersection: A new way of defining records in type theory, in: Proceedings of 8th IEEE Symposium on Logic in Computer Science, 2003, pp. 86–95 A.P. Kopylov, Type theoretical foundations for data structures, classes, and objects, PhD thesis, Cornell University, January 2004 Kreitz, 1999, Automated fast-track reconfiguration of group communication systems, vol. 1579, 104 C. Kreitz, The Nuprl Proof Development System, version 5: Reference Manual and User's Guide, Cornell University, Department of Computer Science, 2002 Kreitz, 2004, Building reliable, high-performance networks with the Nuprl proof development system, J. Funct. Programming, 14, 21, 10.1017/S0956796803004854 Kreitz, 1998, A proof environment for the development of group communication systems, vol. 1421, 317 Kreitz, 1999, Connection-based theorem proving in classical and non-classical logics, J. Universal Comput. Sci., 5, 88 Kreitz, 2000, A uniform procedure for converting matrix proofs into sequent-style systems, J. Inform. Comput., 162, 226, 10.1006/inco.2000.2913 Lamport, 1978, Time, clocks and the ordering of events in a distributed system, Comm. ACM, 21, 558, 10.1145/359545.359563 Lamport, 1986, The mutual exclusion problem, part ii: statement and solutions, J. ACM, 33, 327, 10.1145/5383.5385 Liu, 1999, Building reliable, high-performance communication systems from components, Oper. Syst. Rev., 34, 80, 10.1145/319344.319157 Liu, 2001, Protocol switching: Exploiting meta-properties, 37 Lorigo, 2004, A graph-based approach towards discerning inherent structures in a digital library of formal mathematics, 220 Lynch, 1996 Martin-Löf, 1973, An intuitionistic theory of types: Predicative part, 73 Martin-Löf, 1982, Constructive mathematics and computer programming, 153 Martin-Löf, 1984, Intuitionistic Type Theory, vol. 1 P.F. Mendler, Inductive definition in type theory, PhD thesis, Cornell University, 1988 C. Murthy, A computational analysis of Girard's translation and LC, in: Seventh Symposium on Logic in Computer Science, 1992, pp. 90–101 Murthy, 1990, A constructive proof of Higman's lemma, 257 P. Naumov, Publishing formal mathematics on the web, Technical Report TR98-1689, Cornell University, Department of Computer Science, 1998 Nordström, 1990 Pollack, 2000, Dependently typed records for representing mathematical structure, vol. 1869, 461 Russell, 1908, Mathematical logic as based on a theory of types, Am. J. Math., 30, 222, 10.2307/2369948 L. Page, S. Brin, The anatomy of a large-scale hypertextual (web) search engine, in: Seventh International World Wide Web Conference, 1998 Schmitt, 2001, JProver: Integrating connection-based theorem proving into interactive proof assistants, vol. 2083, 421 Scott, 1976, Data types as lattices, SIAM J. Comput., 5, 522, 10.1137/0205037 Smullyan, 1968 Thompson, 1991 Sjerp Troelstra, 1973, Metamathematical Investigation of Intuitionistic Mathematics, vol. 344 Troelstra, 1988 University of Cambridge, Computer Laboratory, The HOL System: DESCRIPTION, March 1994 Whitehead, 1925 Zimmer, 2002, The Mathweb Software Bus for distributed mathematical reasoning, vol. 1632, 217