Aagaard, M. and Harrison, J. (eds.) (2000) Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000, Volume 1869 of Lecture Notes in Computer Science. Springer-Verlag.
Aichinger, E. (1994) Interpolation with Near-rings of Polynomial Functions. Ph. D. thesis, Johannes Kepler Universität Linz. Author’s Diplomarbeit.
Andersen, F. and Petersen, K. D. (1991) Recursive boolean functions in HOL. See Archer, Joyce, Levitt, and Windley (1991), pp. 367–377.
Archer, M., Joyce, J. J., Levitt, K. N., and Windley, P. J. (eds.) (1991) Proceedings of the 1991 International Workshop on the HOL theorem proving system and its Applications, University of California at Davis, Davis CA, USA. IEEE Computer Society Press.
Baader, F. and Nipkow, T. (1998) Term Rewriting and All That. Cambridge University Press.
Back, R. (1980) Correctness Preserving Program Transformations: Proof Theory and Applications, Volume 131 of Mathematical Centre Tracts. Mathematical Centre, Amsterdam.
Back, R.-J. and von Wright, J. (1998) Refinement Calculus: A Systematic Introduction. Graduate texts in computer science. Springer-Verlag.
Barras, B. (2000) Programming and computing in HOL. See Aagaard and Harrison (2000), pp. 17–37.
Birtwistle, G. and Subrahmanyam, P. A. (eds.) (1989) Current Trends in Hardware Verification and Automated Theorem Proving. Springer-Verlag.
Boolos, G. S. (1995) The Logic of Provability. Cambridge University Press.
Boulton, R. (1992) Boyer-Moore automation for the HOL system. In Claesen, L. J. M. and Gordon, M. J. C. (eds.), Proceedings of the IFIP TC10/WG10.2 International Workshop on Higher Order Logic Theorem Proving and its Applications, Volume A-20 of IFIP Transactions A: Computer Science and Technology, IMEC, Leuven, Belgium, pp. 133–142. North-Holland.
Boulton, R., Gordon, A., Gordon, M., Harrison, J., Herbert, J., and Van Tassel, J. (1993) Experience with embedding hardware description languages in HOL. In Stavridou, V., Melham, T. F., and Boute, R. T. (eds.), Proceedings of the IFIP TC10/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, Volume A-10 of IFIP Transactions A: Computer Science and Technology, Nijmegen, The Netherlands, pp. 129–156. North-Holland.
Boulton, R. J. (1993) Efficiency in a fully-expansive theorem prover. Technical Report 337, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge, CB2 3QG, UK. Author’s PhD thesis.
Boyer, R. S. and Moore, J. S. (1979) A Computational Logic. ACM Monograph Series. Academic Press.
Boyer, R. S. and Moore, J. S. (1981) Metafunctions: proving them correct and using them efficiently as new proof procedures. In Boyer, R. S. and Moore, J. S. (eds.), The Correctness Problem in Computer Science, pp. 103–184. Academic Press.
Bryant, R. E. (1991) A method for hardware verification based on logic simulation. Journal of the ACM, 38, 299–328.
Carnap, R. (1937) The Logical Syntax of Language. International library of psychology, philosophy and scientific method. Routledge & Kegan Paul. Translated from ‘Logische Syntax der Sprache’ by Amethe Smeaton (Countess von Zeppelin), with some new sections not in the German original.
Church, A. (1940) A formulation of the Simple Theory of Types. Journal of Symbolic Logic, 5, 56–68.
Clarke, E., Grumberg, O., and Hamaguchi, K. (1994) Another look at LTL model checking. In Dill, D. L. (ed.), Proceedings of the Sixth International Conference on Computer-Aided Verification (CAV’94), Volume 818 of Lecture Notes in Computer Science, pp. 415–427. Springer-Verlag.
Colmerauer, A. (1990) An introduction to Prolog III. Communications of the ACM, 33(7), 69–90.
Cooper, D. C. (1972) Theorem proving in arithmetic without multiplication. In Melzer, B. and Michie, D. (eds.), Machine Intelligence 7, pp. 91–99. Elsevier.
de Bruijn, N. G. (1980) A survey of the project AUTOMATH. In Seldin, J. P. and Hindley, J. R. (eds.), To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism, pp. 589–606. Academic Press.
DePree, J. and Swartz, C. (1988) Introduction to Real Analysis. Wiley.
Devaney, R. L. (1987) An Introduction to Chaotic Dynamical Systems. Addison-Wesley.
Dijkstra, E. W. (1976) A Discipline of Programming. Prentice-Hall.
Dijkstra, E. W. (1989) On an exercise of Tony Hoare’s. Available on the Web as www.cs.utexas.edu/users/EWD/ewd10xx/EWD1062.PDF.
Dijkstra, E. W. (2000) The notational conventions I adopted, and why (EWD 1300). Available on the Web as www.cs.utexas.edu/users/EWD/ewd13xx/EWD1300.PDF.
Dijkstra, E. W. and Scholten, C. S. (1990) Predicate Calculus and Program Semantics. Springer-Verlag.
Enderton, H. B. (1972) A Mathematical Introduction to Logic. Academic Press.
Floyd, R. W. (1967) Assigning meanings to programs. In Proceedings of AMS Symposia in Applied Mathematics, 19: Mathematical Aspects of Computer Science, pp. 19–32. American Mathematical Society.
Forster, T. (2003) Reasoning about theoretical entities, Volume 3 of Advances in Logic. World Scientific.
Gordon, M. (1985) Why higher-order logic is a good formalism for specifying and verifying hardware. Technical Report 77, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge, CB2 3QG, UK.
Gordon, M. J. C. (1982) Representing a logic in the LCF metalanguage. In Néel, D. (ed.), Tools and notions for program construction: an advanced course, pp. 163–185. Cambridge University Press.
Gordon, M. J. C. (1989) Mechanizing programming logics in higher order logic. See Birtwistle and Subrahmanyam (1989), pp. 387–439.
Gordon, M. J. C. and Melham, T. F. (1993) Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press.
Gordon, M. J. C., Milner, R., and Wadsworth, C. P. (1979) Edinburgh LCF: A Mechanised Logic of Computation, Volume 78 of Lecture Notes in Computer Science. Springer-Verlag.
Graham, B. T. (1992) The SECD Microprocessor: A verification case study, Volume 178 of Kluwer international series in engineering and computer science. Kluwer Academic Publishers.
Guangxing, Z. and Xiaoning, Z. (2004) An effective decision method for semidefinite polynomials. Journal of Symbolic Computation, 37, 83–99.
Guard, J. R., Oglesby, F. C., Bennett, J. H., and Settle, L. G. (1969) Semi-automated mathematics. Journal of the ACM, 16, 49–62.
Hanna, F. K. and Daeche, N. (1986) Specification and verification using higher-order logic: A case study. In Milne, G. and Subrahmanyam, P. A. (eds.), Formal Aspects of VLSI Design: Proceedings of the 1985 Edinburgh Workshop on VLSI, pp. 179–213.
Hardy, G. H. and Wright, E. M. (1979) An Introduction to the Theory of Numbers (5th ed.). Clarendon Press.
Harrison, J. (1996a) HOL Light: A tutorial introduction. In Srivas, M. and Camilleri, A. (eds.), Proceedings of the First International Conference on Formal Methods in Computer-Aided Design (FMCAD’96), Volume 1166 of Lecture Notes in Computer Science, pp. 265–269. Springer-Verlag.
Harrison, J. (1996b) A Mizar mode for HOL. See Wright, Grundy, and Harrison (1996), pp. 203–220.
Harrison, J. (1996c) Proof style. In Giménez, E. and Paulin-Mohring, C. (eds.), Types for Proofs and Programs: International Workshop TYPES’96, Volume 1512 of Lecture Notes in Computer Science, Aussois, France, pp. 154–172. Springer-Verlag.
Harrison, J. (1996d) Stålmarck’s algorithm as a HOL derived rule. See Wright, Grundy, and Harrison (1996), pp. 221–234.
Harrison, J. (2000a) Formal verification of floating point trigonometric functions. In Hunt, W. A. and Johnson, S. D. (eds.), Formal Methods in Computer-Aided Design: Third International Conference FMCAD 2000, Volume 1954 of Lecture Notes in Computer Science, pp. 217–233. Springer-Verlag.
Harrison, J. (2000b) Formal verification of IA-64 division algorithms. See Aagaard and Harrison (2000), pp. 234–251.
Harrison, J. (2003) Formal verification of square root algorithms. Formal Methods in System Design, 22, 143–153.
Harrison, J. and Slind, K. (1994) A reference
version of HOL. Presented in poster session of 1994 HOL Users Meeting and only
published in participants’ supplementary proceedings. Available on the Web from
http://www.dcs.glasgow.ac.uk/~hug94/sproc.html.
Harrison, J. and Théry, L. (1998) A sceptic’s approach to combining HOL and Maple. Journal of Automated Reasoning, 21, 279–294.
Henson, M. C. (1987) Elements of functional languages. Blackwell Scientific.
Hoare, C. A. R. (1969) An axiomatic basis for computer programming. Communications of the ACM, 12, 576–580, 583.
Homeier, P. V. (2005) A design structure for higher order quotients. In Hurd, J. and Melham, T. (eds.), Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Volume 3603 of Lecture Notes in Computer Science, Oxford, UK, pp. 130–146. Springer-Verlag.
Hurd, J. (1999) Integrating Gandalf and HOL. In Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., and Théry, L. (eds.), Theorem Proving in Higher Order Logics: 12th International Conference, TPHOLs’99, Volume 1690 of Lecture Notes in Computer Science, Nice, France, pp. 311–321. Springer-Verlag.
Johnson, S. D., Miner, P. S., and Camilleri, A. (1994) Studies of the single pulser in various reasoning systems. In Kumar, R. and Kropf, T. (eds.), Theorem Provers in Circuit Design — Theory, Practice and Experience, Second International Conference, TPCD ’94, Volume 901 of Lecture Notes in Computer Science, pp. 126–145. Springer-Verlag.
Knaster, B. (1927) Un théorème sur les fonctions d’ensembles. Annales de la Société Polonaise de Mathématique, 6, 133–134. Volume published in 1928.
Knuth, D. and Bendix, P. (1970) Simple word problems in universal algebras. In Leech, J. (ed.), Computational Problems in Abstract Algebra. Pergamon Press.
Kochen, S. and Specker, E. (1967) The problem of hidden variables in quantum mechanics. Journal of Mathematics and Mechanics, 17, 59–87.
Kripke, S. (1963) Semantical considerations on modal logics. Acta Philosophica Fennica, 16, 83–94.
Kumar, R., Kropf, T., and Schneider, K. (1991) Integrating a first-order automatic prover in the HOL environment. See Archer, Joyce, Levitt, and Windley (1991), pp. 170–176.
Lagarias, J. (1985) The problem and its generalizations. The American Mathematical Monthly, 92, 3–23. Available on the Web as http://www.cecm.sfu.ca/organics/papers/lagarias/index.html.
Lamport, L. (1994) The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16, 872–923.
Landin, P. J. (1966) The next 700 programming languages. Communications of the ACM, 9, 157–166.
Lewis, C. I. and Langford, C. H. (1932) Symbolic Logic (2nd ed.). The Century Co.
Loveland, D. W. (1968) Mechanical theorem-proving by model elimination. Journal of the ACM, 15, 236–251.
Loveland, D. W. (1984) Automated theorem-proving: A quarter-century review. In Bledsoe, W. W. and Loveland, D. W. (eds.), Automated Theorem Proving: After 25 Years, Volume 29 of Contemporary Mathematics, pp. 1–45. American Mathematical Society.
MacKenzie, D. (1995) The automation of proof: A historical and sociological exploration. IEEE Annals of the History of Computing, 17(3), 7–29.
Markstein, P. (2000) IA-64 and Elementary Functions: Speed and Precision. Prentice-Hall.
Martin, U. and Nipkow, T. (1990) Ordered rewriting and confluence. In Stickel, M. E. (ed.), 10th International Conference on Automated Deduction, Volume 449 of Lecture Notes in Computer Science, Kaiserslautern, Federal Republic of Germany, pp. 366–380. Springer-Verlag.
McLaughlin, S. and Harrison, J. (2005) A proof-producing decision procedure for real arithmetic. In Nieuwenhuis, R. (ed.), CADE-20: 20th International Conference on Automated Deduction, proceedings, Volume 3632 of Lecture Notes in Computer Science, Tallinn, Estonia, pp. 295–314. Springer-Verlag.
Melham, T. F. (1989) Automating recursive type definitions in higher order logic. See Birtwistle and Subrahmanyam (1989), pp. 341–386.
Melham, T. F. (1991) A package for inductive relation definitions in HOL. See Archer, Joyce, Levitt, and Windley (1991), pp. 350–357.
Mendelson, E. (1987) Introduction to Mathematical Logic (Third ed.). Mathematics series. Wadsworth and Brooks Cole.
Milner, R. (1972) Implementation and applications of Scott’s logic for computable functions. ACM SIGPLAN Notices, 7(1), 1–6.
Moore, G. H. (1982) Zermelo’s axiom of choice: its origins, development, and influence, Volume 8 of Studies in the history of mathematics and physical sciences. Springer-Verlag.
Morgan, C. (1988) The specification statement. ACM Transactions on Programming Languages and Systems, 10, 403–419.
Muller, J.-M. (2006) Elementary functions: Algorithms and Implementation (2nd ed.). Birkhäuser.
Nipkow, T. (1996) Winskel is (almost) right: Towards a mechanized semantics textbook. In Chandru, V. and Vinay, V. (eds.), Foundations of Software Technology and Theoretical Computer Science, 16th conference, proceedings, Lecture Notes in Computer Science, pp. 180–192. Springer-Verlag.
Obua, S. (2005) Proving bounds for real linear programs in Isabelle/HOL. TPHOLs 2005, to appear.
Parrilo, P. A. (2003) Semidefinite programming relaxations for semialgebraic problems. Mathematical Programming, 96, 293–320.
Paulson, L. C. (1983) A higher-order implementation of rewriting. Science of Computer Programming, 3, 119–149.
Paulson, L. C. (1987) Logic and computation: interactive proof with Cambridge LCF, Volume 2 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press.
Peres, A. (1991) Two simple proofs of the Kochen-Specker theorem. Journal of Physics, A24, 175–178.
Ridge, T. (2005) A mechanically verified, efficient, sound and complete theorem prover for first order logic. Available via http://homepages.inf.ed.ac.uk/s0128214/.
Rivest, R. L., Shamir, A., and Adelman, L. M. (1978) A method for obtaining digital signatures and public-key cryptosystems. Journal of the ACM, 21, 120–126.
Rudnicki, P. (1987) Obvious inferences. Journal of Automated Reasoning, 3, 383–393.
Rudnicki, P. (1992) An overview of the MIZAR project. Available on the Web as http://web.cs.ualberta.ca/~piotr/Mizar/Doc/MizarOverview.ps.
Russell, B. (1919) Introduction to mathematical philosophy. Allen & Unwin.
Scott, D. (1993) A type-theoretical alternative to ISWIM, CUCH, OWHY. Theoretical Computer Science, 121, 411–440. Annotated version of a 1969 manuscript.
Scott, D. and Strachey, C. (1971) Toward a mathematical semantics for computer languages. Programming Research Group Technical Monograph PRG-6, Oxford Univ. Computing Lab.
Slind, K. (1991) An implementation of higher order logic. Technical Report 91-419-03, University of Calgary Computer Science Department, 2500 University Drive N. W., Calgary, Alberta, Canada, TN2 1N4. Author’s Masters thesis.
Slind, K. (1997) Derivation and use of induction schemes in higher-order logic. In Gunter, E. L. and Felty, A. (eds.), Theorem Proving in Higher Order Logics: 10th International Conference, TPHOLs’97, Volume 1275 of Lecture Notes in Computer Science, Murray Hill, NJ, pp. ?–? Springer-Verlag.
Smullyan, R. M. (1992) Gödel’s Incompleteness Theorems, Volume 19 of Oxford Logic Guides. Oxford University Press.
Sokołowski, S. (1983) A note on tactics in LCF. Technical Report CSR-140-83, University of Edinburgh, Department of Computer Science.
Solovay, R. M. (1976) Provability interpretations of modal logic. Israel Journal of Mathematics, 25, 287–304.
Stickel, M. E. (1988) A Prolog Technology Theorem Prover: Implementation by an extended Prolog compiler. Journal of Automated Reasoning, 4, 353–380.
Tarski, A. (1936) Der Wahrheitsbegriff in den formalisierten Sprachen. Studia Philosophica, 1, 261–405. English translation, ‘The Concept of Truth in Formalized Languages’, in Tarski (1956), pp. 152–278.
Tarski, A. (1955) A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5, 285–309.
Tarski, A. (ed.) (1956) Logic, Semantics and Metamathematics. Clarendon Press.
Trybulec, A. and Blair, H. A. (1985) Computer aided reasoning. In Parikh, R. (ed.), Logics of Programs, Volume 193 of Lecture Notes in Computer Science, Brooklyn, pp. 406–412. Springer-Verlag.
Wiedijk, F. (2001) Mizar light for HOL Light. In Boulton, R. J. and Jackson, P. B. (eds.), 14th International Conference on Theorem Proving in Higher Order Logics: TPHOLs 2001, Volume 2152 of Lecture Notes in Computer Science, pp. 378–394. Springer-Verlag.
Winskel, G. (1993) The formal semantics of programming languages: an introduction. Foundations of computing. MIT Press.
Wos, L. (1998) Programs that offer fast, flawless, logical reasoning. Communications of the ACM, 41(6), 87–102.
Wos, L. and Pieper, G. W. (1999) A Fascinating Country in the World of Computing: Your Guide to Automated Reasoning. World Scientific.
Wright, J. v., Grundy, J., and Harrison, J. (eds.) (1996) Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs’96, Volume 1125 of Lecture Notes in Computer Science, Turku, Finland. Springer-Verlag.
Wright, J. v., Hekanaho, J., Luostarinen, P., and Langbacka, T. (1993) Mechanizing some advanced refinement concepts. Formal Methods in System Design, 3, 49–82.