doc-src/Logics/logics.bbl
author paulson
Fri Feb 16 18:00:47 1996 +0100 (1996-02-16)
changeset 1512 ce37c64244c0
parent 1444 23ceb1dc9755
child 1536 efbc887dfefb
permissions -rw-r--r--
Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.
     1 \begin{thebibliography}{10}
     2 
     3 \bibitem{abrial93}
     4 J.~R. Abrial and G.~Laffitte.
     5 \newblock Towards the mechanization of the proofs of some classical theorems of
     6   set theory.
     7 \newblock preprint, February 1993.
     8 
     9 \bibitem{andrews86}
    10 Peter~B. Andrews.
    11 \newblock {\em An Introduction to Mathematical Logic and Type Theory: To Truth
    12   Through Proof}.
    13 \newblock Academic Press, 1986.
    14 
    15 \bibitem{basin91}
    16 David Basin and Matt Kaufmann.
    17 \newblock The {Boyer-Moore} prover and {Nuprl}: An experimental comparison.
    18 \newblock In {G\'erard} Huet and Gordon Plotkin, editors, {\em Logical
    19   Frameworks}, pages 89--119. Cambridge University Press, 1991.
    20 
    21 \bibitem{boyer86}
    22 Robert Boyer, Ewing Lusk, William McCune, Ross Overbeek, Mark Stickel, and
    23   Lawrence Wos.
    24 \newblock Set theory in first-order logic: Clauses for {G\"odel's} axioms.
    25 \newblock {\em Journal of Automated Reasoning}, 2(3):287--327, 1986.
    26 
    27 \bibitem{camilleri92}
    28 J.~Camilleri and T.~F. Melham.
    29 \newblock Reasoning with inductively defined relations in the {HOL} theorem
    30   prover.
    31 \newblock Technical Report 265, Computer Laboratory, University of Cambridge,
    32   August 1992.
    33 
    34 \bibitem{church40}
    35 Alonzo Church.
    36 \newblock A formulation of the simple theory of types.
    37 \newblock {\em Journal of Symbolic Logic}, 5:56--68, 1940.
    38 
    39 \bibitem{coen92}
    40 Martin~D. Coen.
    41 \newblock {\em Interactive Program Derivation}.
    42 \newblock PhD thesis, University of Cambridge, November 1992.
    43 \newblock Computer Laboratory Technical Report 272.
    44 
    45 \bibitem{constable86}
    46 R.~L. Constable et~al.
    47 \newblock {\em Implementing Mathematics with the Nuprl Proof Development
    48   System}.
    49 \newblock Prentice-Hall, 1986.
    50 
    51 \bibitem{davey&priestley}
    52 B.~A. Davey and H.~A. Priestley.
    53 \newblock {\em Introduction to Lattices and Order}.
    54 \newblock Cambridge University Press, 1990.
    55 
    56 \bibitem{devlin79}
    57 Keith~J. Devlin.
    58 \newblock {\em Fundamentals of Contemporary Set Theory}.
    59 \newblock Springer, 1979.
    60 
    61 \bibitem{dummett}
    62 Michael Dummett.
    63 \newblock {\em Elements of Intuitionism}.
    64 \newblock Oxford University Press, 1977.
    65 
    66 \bibitem{dyckhoff}
    67 Roy Dyckhoff.
    68 \newblock Contraction-free sequent calculi for intuitionistic logic.
    69 \newblock {\em Journal of Symbolic Logic}, 57(3):795--807, 1992.
    70 
    71 \bibitem{felty91a}
    72 Amy Felty.
    73 \newblock A logic program for transforming sequent proofs to natural deduction
    74   proofs.
    75 \newblock In Peter Schroeder-Heister, editor, {\em Extensions of Logic
    76   Programming}, LNAI 475, pages 157--178. Springer, 1991.
    77 
    78 \bibitem{frost93}
    79 Jacob Frost.
    80 \newblock A case study of co-induction in {Isabelle HOL}.
    81 \newblock Technical Report 308, Computer Laboratory, University of Cambridge,
    82   August 1993.
    83 
    84 \bibitem{gallier86}
    85 J.~H. Gallier.
    86 \newblock {\em Logic for Computer Science: Foundations of Automatic Theorem
    87   Proving}.
    88 \newblock Harper \& Row, 1986.
    89 
    90 \bibitem{mgordon-hol}
    91 M.~J.~C. Gordon and T.~F. Melham.
    92 \newblock {\em Introduction to {HOL}: A Theorem Proving Environment for Higher
    93   Order Logic}.
    94 \newblock Cambridge University Press, 1993.
    95 
    96 \bibitem{halmos60}
    97 Paul~R. Halmos.
    98 \newblock {\em Naive Set Theory}.
    99 \newblock Van Nostrand, 1960.
   100 
   101 \bibitem{huet78}
   102 G.~P. Huet and B.~Lang.
   103 \newblock Proving and applying program transformations expressed with
   104   second-order patterns.
   105 \newblock {\em Acta Informatica}, 11:31--55, 1978.
   106 
   107 \bibitem{kunen80}
   108 Kenneth Kunen.
   109 \newblock {\em Set Theory: An Introduction to Independence Proofs}.
   110 \newblock North-Holland, 1980.
   111 
   112 \bibitem{alf}
   113 Lena Magnusson and Bengt {Nordstr\"om}.
   114 \newblock The {ALF} proof editor and its proof engine.
   115 \newblock In Henk Barendregt and Tobias Nipkow, editors, {\em Types for Proofs
   116   and Programs: International Workshop {TYPES '93}}, LNCS 806, pages 213--237.
   117   Springer, published 1994.
   118 
   119 \bibitem{mw81}
   120 Zohar Manna and Richard Waldinger.
   121 \newblock Deductive synthesis of the unification algorithm.
   122 \newblock {\em Science of Computer Programming}, 1(1):5--48, 1981.
   123 
   124 \bibitem{martinlof84}
   125 Per Martin-L\"of.
   126 \newblock {\em Intuitionistic type theory}.
   127 \newblock Bibliopolis, 1984.
   128 
   129 \bibitem{milner-coind}
   130 Robin Milner and Mads Tofte.
   131 \newblock Co-induction in relational semantics.
   132 \newblock {\em Theoretical Computer Science}, 87:209--220, 1991.
   133 
   134 \bibitem{noel}
   135 Philippe No{\"e}l.
   136 \newblock Experimenting with {Isabelle} in {ZF} set theory.
   137 \newblock {\em Journal of Automated Reasoning}, 10(1):15--58, 1993.
   138 
   139 \bibitem{nordstrom90}
   140 Bengt {Nordstr\"om}, Kent Petersson, and Jan Smith.
   141 \newblock {\em Programming in {Martin-L\"of}'s Type Theory. An Introduction}.
   142 \newblock Oxford University Press, 1990.
   143 
   144 \bibitem{paulin92}
   145 Christine Paulin-Mohring.
   146 \newblock Inductive definitions in the system {Coq}: Rules and properties.
   147 \newblock Research Report 92-49, LIP, Ecole Normale Sup\'erieure de Lyon,
   148   December 1992.
   149 
   150 \bibitem{paulson85}
   151 Lawrence~C. Paulson.
   152 \newblock Verifying the unification algorithm in {LCF}.
   153 \newblock {\em Science of Computer Programming}, 5:143--170, 1985.
   154 
   155 \bibitem{paulson87}
   156 Lawrence~C. Paulson.
   157 \newblock {\em Logic and Computation: Interactive proof with Cambridge LCF}.
   158 \newblock Cambridge University Press, 1987.
   159 
   160 \bibitem{paulson-coind}
   161 Lawrence~C. Paulson.
   162 \newblock Co-induction and co-recursion in higher-order logic.
   163 \newblock Technical Report 304, Computer Laboratory, University of Cambridge,
   164   July 1993.
   165 \newblock To appear in the Festscrift for Alonzo Church, edited by A. Anderson
   166   and M. Zeleny.
   167 
   168 \bibitem{paulson-set-I}
   169 Lawrence~C. Paulson.
   170 \newblock Set theory for verification: {I}. {From} foundations to functions.
   171 \newblock {\em Journal of Automated Reasoning}, 11(3):353--389, 1993.
   172 
   173 \bibitem{paulson-CADE}
   174 Lawrence~C. Paulson.
   175 \newblock A fixedpoint approach to implementing (co)inductive definitions.
   176 \newblock In Alan Bundy, editor, {\em Automated Deduction --- {CADE}-12}, LNAI
   177   814, pages 148--161. Springer, 1994.
   178 \newblock 12th international conference.
   179 
   180 \bibitem{paulson-set-II}
   181 Lawrence~C. Paulson.
   182 \newblock Set theory for verification: {II}. {Induction} and recursion.
   183 \newblock {\em Journal of Automated Reasoning}, 15(2):167--215, 1995.
   184 
   185 \bibitem{paulson-COLOG}
   186 Lawrence~C. Paulson.
   187 \newblock A formulation of the simple theory of types (for {Isabelle}).
   188 \newblock In P.~Martin-L\"of and G.~Mints, editors, {\em COLOG-88:
   189   International Conference on Computer Logic}, LNCS 417, pages 246--274,
   190   Tallinn, Published 1990. Estonian Academy of Sciences, Springer.
   191 
   192 \bibitem{paulson-final}
   193 Lawrence~C. Paulson.
   194 \newblock A concrete final coalgebra theorem for {ZF} set theory.
   195 \newblock In Peter Dybjer, Bengt Nordstr{\"om}, and Jan Smith, editors, {\em
   196   Types for Proofs and Programs: International Workshop {TYPES '94}}, LNCS 996,
   197   pages 120--139. Springer, published 1995.
   198 
   199 \bibitem{pelletier86}
   200 F.~J. Pelletier.
   201 \newblock Seventy-five problems for testing automatic theorem provers.
   202 \newblock {\em Journal of Automated Reasoning}, 2:191--216, 1986.
   203 \newblock Errata, JAR 4 (1988), 235--236.
   204 
   205 \bibitem{plaisted90}
   206 David~A. Plaisted.
   207 \newblock A sequent-style model elimination strategy and a positive refinement.
   208 \newblock {\em Journal of Automated Reasoning}, 6(4):389--402, 1990.
   209 
   210 \bibitem{quaife92}
   211 Art Quaife.
   212 \newblock Automated deduction in {von Neumann-Bernays-G\"odel} set theory.
   213 \newblock {\em Journal of Automated Reasoning}, 8(1):91--147, 1992.
   214 
   215 \bibitem{suppes72}
   216 Patrick Suppes.
   217 \newblock {\em Axiomatic Set Theory}.
   218 \newblock Dover, 1972.
   219 
   220 \bibitem{takeuti87}
   221 G.~Takeuti.
   222 \newblock {\em Proof Theory}.
   223 \newblock North-Holland, 2nd edition, 1987.
   224 
   225 \bibitem{thompson91}
   226 Simon Thompson.
   227 \newblock {\em Type Theory and Functional Programming}.
   228 \newblock Addison-Wesley, 1991.
   229 
   230 \bibitem{principia}
   231 A.~N. Whitehead and B.~Russell.
   232 \newblock {\em Principia Mathematica}.
   233 \newblock Cambridge University Press, 1962.
   234 \newblock Paperback edition to *56, abridged from the 2nd edition (1927).
   235 
   236 \bibitem{winskel93}
   237 Glynn Winskel.
   238 \newblock {\em The Formal Semantics of Programming Languages}.
   239 \newblock MIT Press, 1993.
   240 
   241 \end{thebibliography}