Joe Leslie-Hurd's Bibliography

[1] Mark D. Aagaard, Robert B. Jones, and Carl-Johan H. Seger. Combining theorem proving and trajectory evaluation in an industrial environment. In Proceedings of the 1998 Conference on Design Automation (DAC-98), pages 538–541, Los Alamitos, CA, June 1998. ACM/IEEE. [ bib ]
[2] Martin Abadi and Joseph Y. Halpern. Decidability and expressiveness for first-order logics of probability. Information and Computation, 1994. [ bib ]
[3] Iago Abal, Alcino Cunha, Joe Hurd, and Jorge Sousa Pinto. Using term rewriting to solve bit-vector arithmetic problems (poster presentation). In SAT-2012 [573], pages 493–495. [ bib | http ]
[4] Wilhelm Ackermann. Solvable Cases of the Decision Problem. Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, 1954. [ bib ]
[5] Mark Adams. Introducing HOL Zero. In Fukuda et al. [554], pages 142–143. [ bib | Abstract ]
[6] Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Wolfram Menzel, Wolfgang Reif, Gerhard Schellhorn, and Peter H. Schmitt. Integration of automated and interactive theorem proving. In W. Bibel and P. Schmitt, editors, Automated Deduction: A Basis for Applications, volume II, chapter 4, pages 97–116. Kluwer, 1998. [ bib | .ps.gz | Abstract ]
[7] B. Akbarpour and S. Tahar. An approach for the formal verification of DSP designs using theorem proving. IEEE Transactions on CAD of Integrated Circuits and Systems, 25(8):1141–1457, 2006. [ bib | .pdf ]
[8] Torben Amtoft, John Hatcliff, Edwin Rodríguez, Robby, Jonathan Hoag, and David Greve. Specification and checking of software contracts for conditional information flow. In FM-2008 [529]. [ bib | .html ]
[9] R. Anderson. Why information security is hard - an economic perspective. In ACSAC-2001 [503], pages 358–365. [ bib | .pdf | Abstract ]
[10] Ross Anderson. Security Engineering: A Guide to Building Dependable Distributed Systems. Wiley, 1 edition, January 2001. [ bib | .html ]
[11] Tresys Technology. Apol Help Files, 2008. Available from http://oss.tresys.com/projects/setools/wiki/helpFiles/iflow_help. [ bib ]
[12] A. Armando and S. Ranise. From integrated reasoning specialists to “plug-and-play” reasoning components. In Calmet and Plaza [505], pages 42–54. [ bib ]
[13] Alessandro Armando, Silvio Ranise, and Michael Rusinowitch. A rewriting approach to satisfiability procedures. Information and Computation, 183(2):140–164, June 2003. [ bib | .ps ]
[14] R. Arthan, P. Caseley, C. O'Halloran, and A. Smith. ClawZ: Control laws in Z. In ICFEM-2000 [551], pages 169–176. [ bib ]
[15] R. D. Arthan and R. B. Jones. Z in HOL in ProofPower. BCS FACS FACTS, 2005-1. [ bib ]
[16] Owen L. Astrachan and Mark E. Stickel. Caching and lemmaizing in model elimination theorem provers. In Kapur [511], pages 224–238. [ bib | .html ]
[17] O. L. Astrachan and Donald W. Loveland. The use of lemmas in the model elimination procedure. Journal of Automated Reasoning, 19(1):117–141, August 1997. [ bib | .html ]
[18] Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. [ bib ]
[19] Alan Baker. A Concise Introduction to the Theory of Numbers. Cambridge University Press, 1984. [ bib ]
[20] Siani Baker, Andrew Ireland, and Alan Smaill. On the use of the constructive omega-rule within automated deduction. In Voronkov [559], pages 214–225. [ bib | .html | Abstract ]
[21] Michael Baldamus, Klaus Schneider, Michael Wenz, and Roberto Ziller. Can American Checkers be solved by means of symbolic model checking? In Howard Bowman, editor, Formal Methods Elsewhere (a Satellite Workshop of FORTE-PSTV-2000 devoted to applications of formal methods to areas other than communication protocols and software engineering), volume 43 of Electronic Notes in Theoretical Computer Science. Elsevier, May 2001. [ bib | .pdf | Abstract ]
[22] T. Ball, E. Bounimova, B. Cook, V. Levin, J. Lichtenberg, C. McGarvey, B. Ondrusek, S. K. Rajamani, and A. Ustuner. Thorough static analysis of device drivers. In EUROSYS-2006 [527], pages 73–85. [ bib ]
[23] Clemens Ballarin. Locales and locale expressions in Isabelle/Isar. In Berardi et al. [604], pages 34–50. [ bib ]
[24] Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989. [ bib ]
[25] Paul H. Bardell, W. H. McAnney, and J. Savir. Built In Test for VLSI: Pseudorandom Techniques. John Wiley, October 1987. [ bib | .html | Abstract ]
[26] Bruno Barras, Samuel Boutin, Cristina Cornes, Judicael Courant, Jean-Christophe Filliatre, Eduardo Gimenez, Hugo Herbelin, Gérard Huet, César A. Muñoz, Chetan Murthy, Catherine Parent, Christine Paulin-Mohring, Amokrane Saibi, and Benjamin Werner. The Coq proof assistant reference manual: Version 6.1. Technical Report RT-0203, INRIA (Institut National de Recherche en Informatique et en Automatique), France, 1997. [ bib ]
[27] Bruno Barras. Programming and computing in HOL. In Aagaard and Harrison [588], pages 17–37. [ bib ]
[28] Andrej Bauer, Edmund M. Clarke, and Xudong Zhao. Analytica - an experiment in combining theorem proving and symbolic computation. Journal of Automated Reasoning, 21(3):295–325, 1998. [ bib | .ps ]
[29] Bernhard Beckert and Joachim Posegga. leanTAP: Lean tableau-based deduction. Journal of Automated Reasoning, 15(3):339–358, December 1995. [ bib | .ps.Z ]
[30] Michael J. Beeson. Foundations of Constructive Mathematics. Springer, 1985. [ bib ]
[31] Michael Beeson. Unification in Lambda-Calculi with if-then-else. In Kirchner and Kirchner [514], pages 103–118. [ bib | http | Abstract ]
[32] Eric T. Bell. Debunking Science. University of Washington Book Store, 1930. [ bib ]
[33] C. Benzmuller. Equality and Extensionality in Higher-Order Theorem Proving. PhD thesis, Saarland University, April 1999. [ bib | .ps.gz ]
[34] Stefan Berghofer and Tobias Nipkow. Proof terms for simply typed higher order logic. In Aagaard and Harrison [588], pages 38–52. [ bib | .html | Abstract ]
[35] E. R. Berlekamp. Factoring polynomials over large finite fields. Math. Comput., 24, 1970. [ bib | Abstract ]
[36] Tim Berners-Lee, James Hendler, and Ora Lassila. The semantic web. Scientific American, May 2001. [ bib ]
[37] Al Bessey, Ken Block, Ben Chelf, Andy Chou, Bryan Fulton, Seth Hallem, Charles H. Gros, Asya Kamsky, Scott McPeak, and Dawson Engler. A few billion lines of code later: using static analysis to find bugs in the real world. Communications of the ACM, 53(2):66–75, February 2010. [ bib | http ]
[38] Marc Bezem, Dimitri Hendriks, and Hans de Nivelle. Automated proof construction in type theory using resolution. In McAllester [516], pages 148–163. [ bib | http ]
[39] Józef Bialas. The σ-additive measure theory. Journal of Formalized Mathematics, 1990. [ bib | .html ]
[40] Józef Bialas. Properties of Caratheodor's measure. Journal of Formalized Mathematics, 1992. [ bib | .html ]
[41] Ambrose Bierce. The Devil's Dictionary. Dover, dover thrift edition, 1993. [ bib ]
[42] Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Ofer Strichman, and Yunshun Zhu. Bounded Model Checking, volume 58 of Advances in Computers, pages 117–148. Elsevier, August 2003. [ bib | .pdf ]
[43] P. Billingsley. Probability and Measure. John Wiley & Sons, Inc., New York, 2nd edition, 1986. [ bib ]
[44] Jesse Bingham and Joe Leslie-Hurd. Verifying relative error bounds using symbolic simulation. In Biere and Bloem [520], pages 277–292. [ bib | http | Abstract ]
[45] Steven Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, and Keith Wansbrough. The TCP specification: A quick introduction. Available from Peter Sewell's web site, March 2004. [ bib | .ps ]
[46] Ian Blake, Gadiel Seroussi, and Nigel Smart. Elliptic Curves in Cryptography, volume 265 of London Mathematical Society Lecture Note Series. Cambridge University Press, 1999. [ bib ]
[47] Sandrine Blazy and Xavier Leroy. Mechanized semantics for the Clight subset of the C language. Special Issue of the Journal of Automated Reasoning, 43(3):263–288, October 2009. [ bib | http | Abstract ]
[48] E. Bleicher. Freezer and EGT-query service on Nalimov DTM EGTs. Available at the web page http://www.k4it.de, 2006. [ bib ]
[49] Sylvie Boldo and César Muñoz. A high-level formalization of floating-point numbers in PVS. Technical Report NASA/CR-2006-214298, National Aeronautics and Space Administration, Langley Research Center, Hampton VA 23681-2199, USA, October 2006. [ bib | .pdf ]
[50] George Boole. The Mathematical Analysis of Logic, Being an Essay Toward a Calculus of Deductive Reasoning. Macmillan, Cambridge, 1847. [ bib ]
[51] Maksym Bortin, Einar Broch Johnsen, and Christoph Lüth. Structured formal development in Isabelle. Nordic Journal of Computing, 13:1–20, 2006. [ bib | .html | Abstract ]
[52] Richard J. Boulton. Lazy techniques for fully expansive theorem proving. Formal Methods in System Design, 3(1/2):25–47, August 1993. [ bib ]
[53] Richard J. Boulton. Combining decision procedures in the HOL system. In Schubert et al. [548], pages 75–89. [ bib ]
[54] Richard Boulton, Joe Hurd, and Konrad Slind. Computer assisted reasoning: A Festschrift for Michael J. C. Gordon. Special Issue of the Journal of Automated Reasoning, 43(3):237–242, October 2009. [ bib | http ]
[55] François Bourdoncle. Efficient chaotic iteration strategies with widenings. In Bjørner et al. [535], pages 128–141. [ bib | .html | Abstract ]
[56] M. S. Bourzutschky, J. A. Tamplin, and G. McC. Haworth. Chess endgames: 6-man data and strategy. Theoretical Computer Science, 349:140–157, 2005. [ bib ]
[57] Robert S. Boyer and J Strother Moore. Proof checking the RSA public key encryption algorithm. American Mathematical Monthly, 91(3):181–189, 1984. [ bib | .ps.Z ]
[58] Robert S. Boyer and J Strother Moore. Integrating decision procedures into heuristic theorem provers: A case study of linear arithmetic. Machine Intelligence, 11:83–124, 1988. [ bib ]
[59] Robert S. Boyer, N. G. de Bruijn, Gérard Huet, and Andrzej Trybulec. A mechanically proof-checked encyclopedia of mathematics: Should we build one? can we? In Bundy [512], pages 237–251. [ bib ]
[60] Sally A. Browning and Joe Hurd. Cryptol: The language of cryptanalysis (invited talk abstract). In Bernstein and Gaj [576], pages 57–59. [ bib | http ]
[61] Randal E. Bryant. Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys, 24(3):293–318, September 1992. [ bib | .html | Abstract ]
[62] Alan Bundy. Artificial mathematicians. Available from the author's web site, May 1996. [ bib | .ps.gz ]
[63] N. de Bruijn. The mathematical language AUTOMATH, its usage, and some of its extensions. In Symposium on Automatic Demonstration, pages 29–61. Lecture Notes in Mathematics, 125, Springer, 1970. [ bib ]
[64] G. Buffon. Essai d'arithmétique morale. Supplément à l'Histoire Naturelle, 4, 1777. [ bib ]
[65] Alan Bundy. The Computer Modelling of Mathematical Reasoning. Academic Press, 1983. [ bib ]
[66] David Burke, Joe Hurd, John Launchbury, and Aaron Tomb. Trust relationship modeling for software assurance. In FAST-2010 [528]. [ bib | http ]
[67] Michael Burrows, Martín Abadi, and Roger Needham. A logic of authentication. ACM Transactions on Computer Systems, 8(1):18–36, February 1990. [ bib | .pdf | Abstract ]
[68] Rod Burstall and John Darlington. A transformation system for developing recursive programs. Journal of the Association for Computing Machinery, 1, January 1977. [ bib ]
[69] H. Busch. First-order automation for higher-order-logic theorem proving. In Melham and Camilleri [547]. [ bib ]
[70] Ricky W. Butler, George Hagen, Jeffrey M. Maddalon, César Muñoz, Anthony Narkawicz, and Gilles Dowek. How formal methods implels discovery: A short history of an air traffic management project. In Muñoz [563]. [ bib | .pdf ]
[71] O. Caprotti and M. Oostdijk. Formal and efficient primality proofs by use of computer algebra oracles. Journal of Symbolic Computation, 32(1–2):55–70, 2001. Special Issue on Computer Algebra and Mechanized Reasoning. [ bib ]
[72] Víctor A. Carreño and Paul S. Miner. Specification of the IEEE-854 floating-point standard in HOL and PVS. In HOL-1995a [549]. Supplemental proceedings. [ bib | .pdf ]
[73] Orieta Celiku and Annabelle McIver. Cost-based analysis of probabilistic programs mechanised in HOL. Nordic Journal of Computing, 11(2):102–128, 2004. [ bib | .pdf ]
[74] Orieta Celiku and Annabelle McIver. Compositional specification and analysis of cost-based properties in probabilistic programs. In Fitzgerald et al. [533], pages 107–122. [ bib | http ]
[75] Orieta Celiku. Mechanized Reasoning for Dually-Nondeterministic and Probabilistic Programs. PhD thesis, Åbo Akademi University, 2006. [ bib | http ]
[76] Chin-Liang Chang and Richard Char-Tung Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press, New York, 1973. [ bib ]
[77] Alonzo Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56–68, 1940. [ bib ]
[78] Koen Claessen and John Hughes. QuickCheck: a lightweight tool for random testing of Haskell programs. ACM SIGPLAN Notices, 35(9):268–279, September 2000. [ bib | http ]
[79] E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, 1999. [ bib ]
[80] T. Coe. Inside the Pentium FDIV bug. Dr. Dobbs Journal, April 1996. [ bib ]
[81] Avra Cohn. The notion of proof in hardware verification. Journal of Automated Reasoning, 5(2):127–139, 1989. [ bib ]
[82] Bob Colwell and Bob Brennan. Intel's formal verification experience on the Willamette development. In Aagaard and Harrison [588], pages 106–107. [ bib ]
[83] Adriana B. Compagnoni. Higher-Order Subtyping with Intersection Types. PhD thesis, Catholic University, Nigmegen, January 1995. [ bib ]
[84] Stephen A. Cook. The complexity of theorem-proving procedures. In ACM, editor, Third annual ACM Symposium on Theory of Computing, pages 151–158, Shaker Heights, Ohio, USA, May 1971. ACM Press. [ bib ]
[85] Stephen A. Cook. The P versus NP problem. Manuscript prepared for the Clay Mathematics Institute for the Millennium Prize Problems, April 2000. [ bib | http ]
[86] Byron Cook, Andreas Podelski, and Andrey Rybalchenko. Terminator: Beyond safety. In Ball and Jones [519], pages 415–418. [ bib | .html | Abstract ]
[87] Thomas H. Cormen, Charles Eric Leiserson, and Ronald L. Rivest. Introduction to Algorithms. MIT Press/McGraw-Hill, Cambridge, Massachusetts, 1990. [ bib ]
[88] Duncan Coutts, Isaac Potoczny-Jones, and Don Stewart. Haskell: Batteries included. In Gill [538], pages 125–126. [ bib | .html | Abstract ]
[89] D. Craigen, S. Kromodimoeljo, I. Meisels, B. Pase, and M. Saaltink. EVES: An overview. Technical Report CP-91-5402-43, ORA Corporation, 1991. [ bib ]
[90] Paul Curzon. The formal verification of the Fairisle ATM switching element: an overview. Technical Report 328, University of Cambridge Computer Laboratory, March 1994. [ bib ]
[91] David Cyrluk, Patrick Lincoln, and Natarajan Shankar. On Shostak's decision procedure for combinations of theories. In McRobbie and Slaney [513]. [ bib ]
[92] Ingo Dahn and Christoph Wernhard. First order proof problems extracted from an article in the MIZAR mathematical library. In Bonacina and Furbach [536]. [ bib | .html ]
[93] Ingo Dahn. Interpretation of a Mizar-like logic in first-order logic. In Caferra and Salzer [537], pages 116–126. [ bib ]
[94] Marc Daumas, David Lester, and César Muñoz. Verified real number calculations: A library for interval arithmetic. IEEE Transactions on Computers, 58(2):226–237, February 2009. [ bib ]
[95] Harold Davenport. The Higher Arithmetic. Cambridge University Press, sixth edition, 1992. [ bib ]
[96] Morris DeGroot. Probability and Statistics. Addison-Wesley, 2nd edition, 1989. [ bib ]
[97] K. de Leeuw, E. F. Moore, C. E. Shannon, and N. Shapiro. Computability by probabilistic machines. In C. E. Shannon and J. McCarthy, editors, Automata Studies, pages 183–212. Princeton University Press, Princeton, NJ, 1955. [ bib ]
[98] Richard A. De Millo, Richard J. Lipton, and Alan J. Perlis. Social processes and proofs of theorems and programs. Communications of the ACM, 22(5):271–280, 1979. [ bib | DOI | Abstract ]
[99] Ben L. Di Vito. Hypatheon: A mathematical database for PVS users (extended abstract). In Wegner [562]. [ bib | .pdf ]
[100] Louise A. Dennis, Graham Collins, Michael Norrish, Richard Boulton, Konrad Slind, Graham Robinson, Mike Gordon, and Tom Melham. The PROSPER toolkit. In Graf and Schwartzbach [582], pages 78–92. [ bib | .pdf ]
[101] Jörg Denzinger and Dirk Fuchs. Knowledge-based cooperation between theorem provers by TECHS. SEKI-Report SR-97-11, University of Kaiserslautern, 1997. [ bib | .ps.gz ]
[102] Edsger W. Dijkstra. The humble programmer. Communications of the ACM, 15(10):859–866, October 1972. [ bib | http ]
[103] E. W. Dijkstra. A Discipline of Programming. Prentice Hall, 1976. [ bib ]
[104] Eelco Dolstra and Andres Löh. NixOS: A purely functional Linux distribution. In Hook and Thiemann [552], pages 367–378. [ bib | http ]
[105] Theo Drane, Samuel Coward, Mertcan Temel, and Joe Leslie-Hurd. On the systematic creation of faithfully rounded commutative truncated booth multipliers. In ARITH-2024 [506], pages 108–115. [ bib | http | Abstract ]
[106] Jianjun Duan, Joe Hurd, Guodong Li, Scott Owens, Konrad Slind, and Junxing Zhang. Functional correctness proofs of encryption algorithms. In Sutcliffe and Voronkov [560], pages 519–533. [ bib | http ]
[107] Stefan Edelkamp. Symbolic exploration in two-player games: Preliminary results. In The International Conference on AI Planning & Scheduling (AIPS), Workshop on Model Checking, pages 40–48, Toulouse, France, 2002. [ bib | .pdf | Abstract ]
[108] Euclid. Elements, 300B.C. [ bib | .html ]
[109] Euclid. Elements. Dover, 1956. Translated by Sir Thomas L. Heath. [ bib ]
[110] William M. Farmer, Joshua D. Guttman, and F. Javier Thayer. IMPS: An interactive mathematical proof system. Journal of Automated Reasoning, 11:213–248, 1993. [ bib | .html | Abstract ]
[111] William M. Farmer. Theory interpretation in simple type theory. In Heering et al. [544], pages 96–123. [ bib | .pdf ]
[112] William M. Farmer. The seven virtues of simple type theory. Journal of Applied Logic, 6:267–286, 2008. [ bib | .html | Abstract ]
[113] V. A. Feldman and D. Harel. A probabilistic dynamic logic. Journal of Computer and System Sciences, 28(2):193–215, 1984. [ bib ]
[114] Warren E. Ferguson, Jesse Bingham, Levent Erkok, John R. Harrison, and Joe Leslie-Hurd. Digit serial methods with applications to division and square root. IEEE Transactions on Computers, 67(3):449–456, March 2018. [ bib | DOI | http | Abstract ]
[115] James H. Fetzer. Program verification: the very idea. Communications of the ACM, 31(9):1048–1063, 1988. [ bib | DOI | Abstract ]
[116] FIDE. The FIDE Handbook, chapter E.I. The Laws of Chess. FIDE, 2004. Available for download from the FIDE website. [ bib | http ]
[117] C. Fidge and C. Shankland. But what if I don't want to wait forever? Formal Aspects of Computing, to appear in 2003. [ bib ]
[118] M. Fierz, M. Cash, and E. Gilbert. The 2002 world computer-checkers championship. ICGA Journal, 25(3):196–198, 2002. [ bib ]
[119] George S. Fishman. Monte Carlo: Concepts, Algorithms and Applications. Springer, 1996. [ bib ]
[120] J. D. Fleuriot. A Combination of Geometry Theorem Proving and Nonstandard Analysis, with Application to Newton's Principia. Distinguished Dissertations. Springer, 2001. [ bib ]
[121] Anthony Fox. Formal specification and verification of ARM6. In Basin and Wolff [593], pages 25–40. [ bib ]
[122] Anthony Fox. An algebraic framework for verifying the correctness of hardware with input and output: A formalization in HOL. In et al. [518], pages 157–174. [ bib ]
[123] Adam Fuchs, Avik Chaudhuri, and Jeffrey Foster. SCanDroid: Automated security certification of Android applications. Available from the second author's website, 2009. [ bib | http | Abstract ]
[124] Dov M. Gabbay and Hans Jürgen Ohlbach. Quantifier elimination in second–order predicate logic. In Bernhard Nebel, Charles Rich, and William Swartout, editors, Principles of Knowledge Representation and Reasoning (KR92), pages 425–435. Morgan Kaufmann, 1992. [ bib | http | Abstract ]
[125] Chris Gathercole and Peter Ross. Small populations over many generations can beat large populations over few generations in genetic programming. http://www.dai.ed.ac.uk/students/chrisg/, 1997. [ bib ]
[126] J. T. Gill. Computational complexity of probabilistic Turing machines. SIAM Journal on Computing, 6(4):675–695, December 1977. [ bib ]
[127] P. C. Gilmore. A proof method for quantification theory: Its justification and realization. IBM Journal of Research and Development, 4:28–35, 1960. [ bib ]
[128] Jean-Yves Girard. Proofs and types, volume 7 of Cambridge tracts in theoretical computer science. Cambridge University Press, 1989. [ bib ]
[129] K. Gödel. Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme. Monatshefte für Mathematik und Physik, 38:173–198, 1931. [ bib ]
[130] K. Gödel. On Formally Undecidable Propositions of Principia Mathematica and Related Systems. Oliver and Boyd, London, 1962. Translated by B. Meltzer. [ bib ]
[131] J. Goguen and G. Malcolm. Algebraic Semantics of Imperative Programs. MIT Press, Cambridge, Mass., 1st edition, 1996. [ bib ]
[132] E. Goldberg and Y. Novikov. BerkMin: A fast and robust SAT-solver. In Design, Automation, and Test in Europe (DATE '02), pages 142–149, March 2002. [ bib | .pdf ]
[133] Charles M. Goldie and Richard G. E. Pinch. Communication theory, volume 20 of LMS Student Texts. Cambridge University Press, 1991. [ bib ]
[134] Georges Gonthier. A computer-checked proof of the four colour theorem. Available for download at the author's website, 2004. [ bib | .pdf | Abstract ]
[135] M. Gordon, R. Milner, L. Morris, M. Newey, and C. Wadsworth. A Metalanguage for interactive proof in LCF. In POPL-1978 [567], pages 119–130. [ bib ]
[136] M. Gordon, R. Milner, and C. Wadsworth. Edinburgh LCF, volume 78 of Lecture Notes in Computer Science. Springer, 1979. [ bib ]
[137] Mike Gordon. Why Higher-Order Logic is a good formalism for specifying and verifying hardware. Technical Report 77, Computer Laboratory, The University of Cambridge, 1985. [ bib ]
[138] M. J. C. Gordon. Programming Language Theory and its Implementation. Prentice Hall, 1988. [ bib ]
[139] Michael J. C. Gordon. HOL: A proof generating system for higher-order logic. In Graham Birtwistle and P. A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis, pages 73–128. Kluwer Academic Publishers, Boston, 1988. [ bib ]
[140] M. J. C. Gordon. Mechanizing programming logics in higher order logic. In G. Birtwistle and P. A. Subrahmanyam, editors, Current Trends in Hardware Verification and Automated Theorem Proving, pages 387–439. Springer-Verlag, 1989. [ bib | .dvi.gz ]
[141] M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL (A theorem-proving environment for higher order logic). Cambridge University Press, 1993. [ bib ]
[142] Mike Gordon. Merging HOL with set theory: preliminary experiments. Technical Report 353, University of Cambridge Computer Laboratory, November 1994. [ bib | http | Abstract ]
[143] M. J. C. Gordon. Notes on PVS from a HOL perspective. Available from the author's web page, 1996. [ bib | .html | Abstract ]
[144] Michael J. C. Gordon. Reachability programming in HOL98 using BDDs. In Aagaard and Harrison [588], pages 179–196. [ bib | http | Abstract ]
[145] Michael J. C. Gordon. Proof, Language, and Interaction: Essays in Honour of Robin Milner, chapter 6. From LCF to HOL: A Short History. MIT Press, May 2000. [ bib ]
[146] Michael J. C. Gordon. Programming combinations of deduction and BDD-based symbolic calculation. LMS Journal of Computation and Mathematics, 5:56–76, August 2002. [ bib | http | Abstract ]
[147] Michael J. C. Gordon. PuzzleTool : An example of programming computation and deduction. In Carreño et al. [592], pages 214–229. [ bib ]
[148] Mike Gordon, Joe Hurd, and Konrad Slind. Executing the formal semantics of the Accellera Property Specification Language by mechanised theorem proving. In Geist and Tronci [522], pages 200–215. [ bib | http | Abstract ]
[149] Mike Gordon, Juliano Iyoda, Scott Owens, and Konrad Slind. A proof-producing hardware compiler for a subset of higher order logic. In Hurd et al. [597], pages 59–75. [ bib | http ]
[150] M. J. C. Gordon. Specification and verification I, 2009. Course notes available from http://www.cl.cam.ac.uk/~mjcg/Teaching/SpecVer1/SpecVer1.html. [ bib ]
[151] M. J. C. Gordon. Specification and verification II, 2009. Course notes available from http://www.cl.cam.ac.uk/~mjcg/Teaching/SpecVer2/SpecVer2.html. [ bib ]
[152] Daniel Gorenstein, Richard Lyons, and Ronald Solomon. The Classification of the Finite Simple Groups. AMS, 1994. [ bib | http ]
[153] Paul Graunke. Verified safety and information flow of a block device. In SSV-2008 [580], pages 187–202. [ bib | http | Abstract ]
[154] Penny Grubb and Armstrong A. Takang. Software Maintenance: Concepts and Practice. World Scientific Publishing Company, 2nd edition, July 2003. [ bib ]
[155] Elsa Gunter. Doing algebra in simple type theory. Technical Report MS-CIS-89-38, Logic & Computation 09, Department of Computer and Information Science, University of Pennsylvania, 1989. [ bib ]
[156] Joshua D. Guttman, Amy L. Herzog, John D. Ramsdell, and Clement W. Skorupka. Verifying information flow goals in Security-Enhanced Linux. Journal of Computer Security, 13(1):115–134, 2005. [ bib | .pdf ]
[157] Florian Haftmann. From higher-order logic to Haskell: There and back again. In Gallagher and Voigtländer [565], pages 155–158. [ bib | .pdf | Abstract ]
[158] Petr Hájek. Metamathematics of Fuzzy Logic, volume 4 of Trends in Logic. Kluwer Academic Publishers, Dordrecht, August 1998. [ bib | http | Abstract ]
[159] Thomas C. Hales. Introduction to the Flyspeck project. In Coquand et al. [523]. [ bib | http | Abstract ]
[160] Joseph Y. Halpern. An analysis of first-order logics of probability. Artificial Intelligence, 1990. [ bib | http | Abstract ]
[161] Darrel Hankerson, Alfred Menezes, and Scott Vanstone. Guide to Elliptic Curve Cryptography. Springer, 2003. [ bib | http ]
[162] R. W. Hansell. Borel measurable mappings for nonseparable metric spaces. Transactions of the American Mathematical Society, 161:145–169, November 1971. [ bib | http | Abstract ]
[163] G. H. Hardy. A Mathematician's Apology, reprinted with a foreword by C. P. Snow. Cambridge University Press, 1993. [ bib ]
[164] John Harrison. Metatheory and reflection in theorem proving: A survey and critique. Technical Report CRC-053, SRI Cambridge, Millers Yard, Cambridge, UK, 1995. [ bib | .html | Abstract ]
[165] John Harrison. Binary decision diagrams as a HOL derived rule. The Computer Journal, 38:162–170, 1995. [ bib | .html | Abstract ]
[166] John Harrison. Optimizing proof search in model elimination. In McRobbie and Slaney [513], pages 313–327. [ bib | .html | Abstract ]
[167] John Harrison. Formalized mathematics. Technical Report 36, Turku Centre for Computer Science (TUCS), Lemminkäisenkatu 14 A, FIN-20520 Turku, Finland, 1996. [ bib | .html | Abstract ]
[168] John Harrison. A Mizar mode for HOL. In von Wright et al. [583], pages 203–220. [ bib | .html | Abstract ]
[169] John Harrison. Proof style. In Giménex and Paulin-Mohring [603], pages 154–172. [ bib | .html | Abstract ]
[170] John Harrison. HOL light: A tutorial introduction. In Srivas and Camilleri [530], pages 265–269. [ bib | .html | Abstract ]
[171] John Harrison. Floating point verification in HOL light: the exponential function. Technical Report 428, University of Cambridge Computer Laboratory, 1997. [ bib | .html ]
[172] John Harrison. Theorem Proving with the Real Numbers (Distinguished dissertations). Springer, 1998. [ bib | .html ]
[173] John Harrison. The HOL Light Manual (1.0), May 1998. [ bib | http ]
[174] John Harrison. Formalizing Dijkstra. In Grundy and Newey [586], pages 171–188. [ bib | .html ]
[175] John Harrison. A HOL theory of Euclidean space. In Hurd and Melham [596], pages 114–129. [ bib | .html ]
[176] John Harrison. Floating-point verification using theorem proving. In Bernardo and Cimatti [575], pages 211–242. [ bib | .html ]
[177] John Harrison. Verifying nonlinear real formulas via sums of squares. In Schneider and Brandt [598], pages 102–118. [ bib | .html ]
[178] John Harrison. Formalizing basic complex analysis. In Matuszewski and Zalewska [602], pages 151–165. [ bib | .html ]
[179] John Harrison. Formalizing an analytic proof of the prime number theorem. Special Issue of the Journal of Automated Reasoning, 43(3):243–261, October 2009. [ bib | http | Abstract ]
[180] Sergiu Hart, Micha Sharir, and Amir Pnueli. Termination of probabilistic concurrent programs. ACM Transactions on Programming Languages and Systems (TOPLAS), 5(3):356–380, July 1983. [ bib ]
[181] O. Hasan and S. Tahar. Formalization of the standard uniform random variable. Theoretical Computer Science, 2007. To appear. [ bib ]
[182] G. McC. Haworth. 6-man chess solved. ICGA Journal, 28(3):153, September 2005. [ bib ]
[183] G. McC. Haworth. Freezer analysis of KRP(a2)KbBP(a3). Private communication, 2006. [ bib ]
[184] Jifeng He, K. Seidel, and A. McIver. Probabilistic models for the guarded command language. Science of Computer Programming, 28(2–3):171–192, April 1997. [ bib ]
[185] E. A. Heinz. Endgame databases and efficient index schemes. ICCA Journal, 22(1):22–32, March 1999. [ bib | .ps.gz | Abstract ]
[186] Jörg Heitkötter and David Beasley. The hitch-hiker's guide to evolutionary computation: A list of frequently asked questions (faq). USENET: comp.ai.genetic, 1998. [ bib | ftp ]
[187] Heber Herencia-Zapana, George Hagen, and Anthony Narkawicz. Formalizing probabilistic safety claims. In Bobaru et al. [564], pages 162–176. [ bib ]
[188] H. J. van den Herik, I. S. Herschberg, and N. Nakad. A six-men-endgame database: KRP(a2)KbBP(a3). ICCA Journal, 10(4):163–180, 1987. [ bib ]
[189] H. J. van den Herik, I. S. Herschberg, and N. Nakad. A reply to R. Sattler's remarks on the KRP(a2)-KbBP(a3) database. ICCA Journal, 11(2/3):88–91, 1988. [ bib ]
[190] Ted Herman. Probabilistic self-stabilization. Information Processing Letters, 35(2):63–67, June 1990. [ bib ]
[191] Thai Son Hoang, Z. Jin, K. Robinsion, A. K. McIver, and C. C. Morgan. Probabilistic invariants for probabilistic machines. In Proceedings of the 3rd International Conference of B and Z users, volume 2651 of Lecture Notes in Computer Science, pages 240–259. Springer, 2003. [ bib ]
[192] Tony Hoare. The verifying compiler. Sample submission for the Workshop on Grand Challenges for Computing Research, November 2002. [ bib | .pdf ]
[193] Peter V. Homeier and David F. Martin. A mechanically verified verification condition generator. The Computer Journal, 38(2):131–141, July 1995. [ bib | .pdf ]
[194] Peter V. Homeier. The HOL-Omega logic. In Berghofer et al. [601], pages 244–259. [ bib | .pdf ]
[195] David Hooper and Kenneth Whyld. The Oxford Companion to Chess. Oxford University Press, 2nd edition, September 1992. [ bib ]
[196] John E. Hopcroft, Rajeev Motwani, and Jeffrey D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 2nd edition, 2001. [ bib ]
[197] Gérard Huet and Derek Oppen. Equations and rewrite rules: A survey. Technical Report CSL-111, SRI International, January 1980. [ bib ]
[198] Brian Huffman. Formal verification of monad transformers. In Thiemann and Findler [553]. [ bib | .html ]
[199] J. Hughes. Why functional programming matters. Computer Journal, 32(2):98–107, 1989. [ bib | .html ]
[200] Marieke Huisman. Reasoning about Java Programs in higher order logic with PVS and Isabelle. PhD thesis, University of Nijmegen, Holland, February 2001. [ bib ]
[201] Joe Hurd. The Real Number Theories in hol98, November 1998. Part of the documentation for the hol98 theorem prover. [ bib | Abstract ]
[202] Joe Hurd. Integrating Gandalf and HOL. In Bertot et al. [587], pages 311–321. [ bib | http | Abstract ]
[203] Joe Hurd. Integrating Gandalf and HOL. Technical Report 461, University of Cambridge Computer Laboratory, May 1999. Second edition. [ bib | .html ]
[204] Joe Hurd. Congruence classes with logic variables. In Aagaard et al. [589], pages 87–101. [ bib ]
[205] Joe Hurd. Lightweight probability theory for verification. In Aagaard et al. [589], pages 103–113. [ bib | Abstract ]
[206] Joe Hurd. The Probability Theories in hol98, June 2000. Part of the documentation for the hol98 theorem prover. [ bib | Abstract ]
[207] Joe Hurd. Congruence classes with logic variables. Logic Journal of the IGPL, 9(1):59–75, January 2001. [ bib | http | Abstract ]
[208] Joe Hurd. Predicate subtyping with predicate sets. In Boulton and Jackson [590], pages 265–280. [ bib | http | Abstract ]
[209] Joe Hurd. Verification of the Miller-Rabin probabilistic primality test. In Boulton and Jackson [591], pages 223–238. [ bib ]
[210] Joe Hurd. Formal Verification of Probabilistic Algorithms. PhD thesis, University of Cambridge, 2002. [ bib | http | Abstract ]
[211] Joe Hurd. A formal approach to probabilistic termination. In Carreño et al. [592], pages 230–245. [ bib | http | Abstract ]
[212] Joe Hurd. HOL theorem prover case study: Verifying probabilistic programs. In Norman et al. [509], pages 83–92. [ bib | Abstract ]
[213] Joe Hurd. Fast normalization in the HOL theorem prover. In Walsh [507]. An extended abstract. [ bib | http ]
[214] Joe Hurd. An LCF-style interface between HOL and first-order logic. In Voronkov [517], pages 134–138. [ bib | http ]
[215] Joe Hurd. Verification of the Miller-Rabin probabilistic primality test. Journal of Logic and Algebraic Programming, 50(1–2):3–21, May–August 2003. Special issue on Probabilistic Techniques for the Design and Analysis of Systems. [ bib | http | Abstract ]
[216] Joe Hurd. Using inequalities as term ordering constraints. Technical Report 567, University of Cambridge Computer Laboratory, June 2003. [ bib | http | Abstract ]
[217] Joe Hurd. Formal verification of probabilistic algorithms. Technical Report 566, University of Cambridge Computer Laboratory, May 2003. [ bib | .html ]
[218] Joe Hurd. First-order proof tactics in higher-order logic theorem provers. In Archer et al. [581], pages 56–68. [ bib | http | Abstract ]
[219] Joe Hurd, Annabelle McIver, and Carroll Morgan. Probabilistic guarded commands mechanized in HOL. In Cerone and Pierro [571], pages 95–111. [ bib ]
[220] Joe Hurd. Compiling HOL4 to native code. In Slind [595]. [ bib | http | Abstract ]
[221] Joe Hurd. Formal verification of chess endgame databases. In Hurd et al. [597], pages 85–100. [ bib | http | Abstract ]
[222] Joe Hurd. Formalizing elliptic curve cryptography in higher order logic. Available from the author's website, October 2005. [ bib | http | Abstract ]
[223] Joe Hurd, Annabelle McIver, and Carroll Morgan. Probabilistic guarded commands mechanized in HOL. Theoretical Computer Science, 346:96–112, November 2005. [ bib | http | Abstract ]
[224] Joe Hurd. First order proof for higher order theorem provers (abstract). In Benzmueller et al. [526], pages 1–3. [ bib ]
[225] Joe Hurd. System description: The Metis proof tactic. In Benzmueller et al. [526], pages 103–104. [ bib ]
[226] Joe Hurd, Mike Gordon, and Anthony Fox. Formalized elliptic curve cryptography. In HCSS-2006 [540]. [ bib | http | Abstract ]
[227] Joe Hurd. Book review: Rippling: Meta-level guidance for mathematical reasoning by A. Bundy, D. Basin, D. Hutter and A. Ireland. Bulletin of Symbolic Logic, 12(3):498–499, 2006. [ bib | http ]
[228] Joe Hurd. Embedding Cryptol in higher order logic. Available from the author's website, March 2007. [ bib | http | Abstract ]
[229] Joe Hurd. Proof pearl: The termination analysis of TERMINATOR. In Schneider and Brandt [598], pages 151–156. [ bib | http | Abstract ]
[230] Joe Hurd, Anthony Fox, Mike Gordon, and Konrad Slind. ARM verification (abstract). In HCSS-2007 [541]. [ bib | http ]
[231] Joe Hurd. OpenTheory: Package management for higher order logic theories. In Reis and Théry [566], pages 31–37. [ bib | http | Abstract ]
[232] Joe Hurd, Magnus Carlsson, Sigbjorn Finne, Brett Letner, Joel Stanley, and Peter White. Policy DSL: High-level specifications of information flows for security policies. In HCSS-2009 [542]. [ bib | http | Abstract ]
[233] Joe Hurd and Guy Haworth. Data assurance in opaque computations. In Van den Herik and Spronck [501], pages 221–231. [ bib | http | Abstract ]
[234] Joe Hurd. Composable packages for higher order logic theories. In Aderhold et al. [605]. [ bib | http | Abstract ]
[235] Joe Hurd. Evaluation opportunities in mechanized theories (invited talk abstract). In McGuinness et al. [525]. [ bib | http ]
[236] Joe Hurd. OpenTheory Article Format, August 2010. Available for download at http://www.gilith.com/opentheory/article.html. [ bib | .html ]
[237] Joe Hurd. The OpenTheory standard theory library. In Bobaru et al. [564], pages 177–191. [ bib | http | Abstract ]
[238] Joe Hurd. FUSE: Inter-application security for android (abstract). In Launchbury and Richards [543], pages 53–54. [ bib | http ]
[239] Michael Huth. The interval domain: A matchmaker for aCTL and aPCTL. In Rance Cleaveland, Michael Mislove, and Philip Mulry, editors, US - Brazil Joint Workshops on the Formal Foundations of Software Systems, volume 14 of Electronic Notes in Theoretical Computer Science. Elsevier, 2000. [ bib | .html ]
[240] Graham Hutton and Erik Meijer. Monadic parser combinators. Technical Report NOTTCS-TR-96-4, Department of Computer Science, University of Nottingham, 1996. [ bib | http | Abstract ]
[241] Paul B. Jackson. Expressive typing and abstract theories in Nuprl and PVS (tutorial). In von Wright et al. [583]. [ bib | .ps.gz | Abstract ]
[242] Mateja Jamnik, Alan Bundy, and Ian Green. On automating diagrammatic proofs of arithmetic arguments. Journal of Logic, Language and Information, 8(3):297–321, 1999. Also available as Department of Artificial Intelligence Research Paper No. 910. [ bib | .ps ]
[243] Claus Skaanning Jensen, Augustine Kong, and Uffe Kjaerulff. Blocking Gibbs sampling in very large probabilistic expert systems. Technical Report R-93-2031, Aalborg University, October 1993. [ bib ]
[244] D. S. Johnson. A catalog of complexity classes. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, Volume A: Algorithms and Complexity, chapter 9, pages 67–161. Elsevier and The MIT Press (co-publishers), 1990. [ bib | Abstract ]
[245] Peter T. Johnstone. Notes on logic and set theory. Cambridge University Press, 1987. [ bib ]
[246] Claire Jones. Probabilistic Non-Determinism. PhD thesis, University of Edinburgh, 1990. [ bib | http ]
[247] Michael D. Jones. Restricted types for HOL. In Gunter [585]. [ bib | .html ]
[248] F. Kammüller and L. C. Paulson. A formal proof of Sylow's first theorem – an experiment in abstract algebra with Isabelle HOL. Journal of Automated Reasoning, 23(3-4):235–264, 1999. [ bib ]
[249] F. Kammüller. Modular reasoning in Isabelle. In McAllester [516]. [ bib ]
[250] David R. Karger. Global min-cuts in RNC, and other ramifications of a simple min-cut algorithm. In Proceedings of the 4th Annual ACM-SIAM Symposium on Discrete Algorithms (SODA '93), pages 21–30, Austin, TX, USA, January 1993. SIAM. [ bib ]
[251] R. M. Karp. The probabilistic analysis of some combinatorial search algorithms. In Traub [453], pages 1–20. [ bib ]
[252] Matt Kaufmann and J Strother Moore. An industrial strength theorem prover for a logic based on Common Lisp. IEEE Transactions on Software Engineering, 23(4):203–213, April 1997. [ bib | http ]
[253] Matt Kaufmann and J Strother Moore. A precise description of the ACL2 logic, 1998. [ bib | .ps.Z ]
[254] Matt Kaufmann, Panagiotis Manolios, and J Strother Moore. Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, June 2000. [ bib ]
[255] Matt Kaufmann, Panagiotis Manolios, and J Strother Moore, editors. Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Publishers, June 2000. [ bib ]
[256] F. P. Kelly. Notes on effective bandwidths. In F.P. Kelly, S. Zachary, and I.B. Ziedins, editors, Stochastic Networks: Theory and Applications, number 4 in Royal Statistical Society Lecture Notes Series, pages 141–168. Oxford University Press, 1996. [ bib ]
[257] H. J. Keisler. Probability quantifiers. In J. Barwise and S. Feferman, editors, Model-Theoretic Logics, pages 509–556. Springer, New York, 1985. [ bib ]
[258] D. J. King and R. D. Arthan. Development of practical verification tools. ICL Systems Journal, 11(1), May 1996. [ bib | .html | Abstract ]
[259] Steve King, Jonathan Hammond, Rod Chapman, and Andy Pryor. Is proof more cost-effective than testing? IEEE Transactions on Software Engineering, 26(8):675–686, August 2000. [ bib | Abstract ]
[260] Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: Formal verification of an OS kernel. In Matthews and Anderson [578], pages 207–220. [ bib | http | Abstract ]
[261] D. E. Knuth and P. B. Bendix. Simple word problems in universal algebra. In J. Leech, editor, Computational problems in abstract algebra, pages 263–297. Pergamon Press, Elmsford, N.Y., 1970. [ bib ]
[262] Donald E. Knuth and Andrew C. Yao. The complexity of nonuniform random number generation. In Traub [453]. [ bib ]
[263] Donald E. Knuth. The Art of Computer Programming: Seminumerical Algorithms. Addison-Wesley, 1997. Third edition. [ bib ]
[264] Neal Koblitz. A Course in Number Theory and Cryptography. Number 114 in Graduate Texts in Mathematics. Springer, 1987. [ bib ]
[265] Andrei N. Kolmogorov. Foundations of the Theory of Probability. Chelsea, New York, 1950. [ bib ]
[266] E. A. Komissarchik and A. L. Futer. Ob analize ferzevogo endshpilia pri pomoshchi EVM. Problemy Kybernet, 29:211–220, 1974. [ bib ]
[267] Konstantin Korovin and Andrei Voronkov. Knuth-Bendix constraint solving is NP-complete. In Orejas et al. [550], pages 979–992. [ bib ]
[268] Dexter Kozen. Semantics of probabilistic programs. In 20th Annual Symposium on Foundations of Computer Science, pages 101–114, Long Beach, Ca., USA, October 1979. IEEE Computer Society Press. [ bib ]
[269] Dexter Kozen. A probabilistic PDL. In Proceedings of the 15th ACM Symposium on Theory of Computing, 1983. [ bib ]
[270] Dexter Kozen. Efficient code certification. Technical Report 98-1661, Cornell University, January 1998. [ bib ]
[271] Jesper Torp Kristensen. Generation and compression of endgame tables in chess with fast random access using OBDDs. Master's thesis, University of Aarhus, Department of Computer Science, February 2005. [ bib | http ]
[272] R. Kumar, T. Kropf, and K. Schneider. Integrating a first-order automatic prover in the HOL environment. In Archer et al. [545], pages 170–176. [ bib ]
[273] Ramana Kumar and Joe Hurd. Standalone tactics using OpenTheory. In Beringer and Felty [556], pages 405–411. [ bib | http | Abstract ]
[274] Ramana Kumar. Challenges in using OpenTheory to transport Harrison's HOL model from HOL Light to HOL4. In Blanchette and Urban [570], pages 110–116. [ bib | http | Abstract ]
[275] Eyal Kushilevitz and Michael O. Rabin. Randomized mutual exclusion algorithms revisited. In Maurice Herlihy, editor, Proceedings of the 11th Annual Symposium on Principles of Distributed Computing, pages 275–283, Vancouver, BC, Canada, August 1992. ACM Press. [ bib ]
[276] Marta Kwiatkowska, Gethin Norman, Roberto Segala, and Jeremy Sproston. Automatic verification of real-time systems with discrete probability distributions. In Katoen [508], pages 75–95. [ bib | .ps.gz | Abstract ]
[277] M. Kwiatkowska, G. Norman, and D. Parker. Prism: Probabilistic symbolic model checker. In Proceedings of PAPM/PROBMIV 2001 Tools Session, September 2001. [ bib | .ps.gz ]
[278] B. A. LaMacchia and A. M. Odlyzko. Computation of discrete logarithms in prime fields. Designs, Codes, and Cryptography, 1(1):46–62, May 1991. [ bib | .html | Abstract ]
[279] Leslie Lamport. How to write a proof, February 1993. [ bib | http | Abstract ]
[280] Leslie Lamport. Latex: A document preparation system. Addison-Wesley, 2nd edition, 1994. [ bib ]
[281] Leslie Lamport and Lawrence C. Paulson. Should your specification language be typed? ACM Transactions on Programming Languages and Systems, 21(3):502–526, May 1999. [ bib | http | Abstract ]
[282] Bruce M. Landman and Aaron Robertson. Ramsey Theory on the Integers. American Mathematical Society, February 2004. [ bib ]
[283] John Launchbury and Simon L. Peyton Jones. Lazy functional state threads. In SIGPLAN Symposium on Programming Language Design and Implementation (PLDI'94), Orlando, pages 24–35, June 1994. [ bib ]
[284] Jeff Lawson. Operational code authentication, 1999. [ bib | .html ]
[285] Meir M. Lehman. Programs, life cycles, and laws of software evolution. Proceedings of the IEEE, 68(9):1060–1076, 1980. [ bib | .pdf ]
[286] Douglas B. Lenat. CYC: A large-scale investment in knowledge infrastructure. Communications of the ACM, 38(11):33–38, 1995. [ bib | .html ]
[287] H. W. Lenstra. Factoring integers with elliptic curves. Ann. Math., 126:649–673, 1987. [ bib ]
[288] Xavier Leroy. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In Morrisett and Jones [569], pages 42–54. [ bib | .pdf ]
[289] Joe Leslie-Hurd and Guy Haworth. Computer theorem proving and HoTT. ICGA Journal, 36(2):100–103, June 2013. [ bib | http | Abstract ]
[290] Joe Leslie-Hurd. Maintaining verified software. In Shan [539], pages 71–80. [ bib | http | Abstract ]
[291] Clarence Irving Lewis. A Survey of Symbolic Logic. Univ. of California Press, Berkeley, Berkeley, 1918. Reprint of Chapters I–IV by Dover Publications, 1960, New York. [ bib ]
[292] J. R. Lewis and B. Martin. Cryptol: High assurance, retargetable crypto development and validation. In MILCOM-2003 [561], pages 820–825. [ bib | http | Abstract ]
[293] Guodong Li and Konrad Slind. An embedding of Cryptol in HOL-4. Unpublished draft, 2005. [ bib ]
[294] Donald W. Loveland. Mechanical theorem proving by model elimination. Journal of the ACM, 15(2):236–251, April 1968. [ bib ]
[295] Christopher Lynch and Barbara Morawska. Goal-directed E-unification. In RTA-2001 [572], pages 231–245. [ bib | .ps | Abstract ]
[296] Christopher Lynch and Barbara Morawska. Goal-directed E-unification. In RTA-2001 [572], pages 231–245. [ bib | .ps | Abstract ]
[297] Donald MacKenzie. Mechanizing proof: computing, risk, and trust. MIT Press, 2001. [ bib ]
[298] David MacQueen. Modules for Standard ML. In Boyer et al. [557], pages 198–207. [ bib | .pdf | Abstract ]
[299] Jeffrey M. Maddalon, Ricky W. Butler, and César Muñoz. A mathematical basis for the safety analysis of conflict prevention algorithms. Technical Report NASA/TM-2009-215768, National Aeronautics and Space Administration, Langley Research Center, Hampton VA 23681-2199, USA, June 2009. [ bib | .pdf ]
[300] Harry G. Mairson. Deciding ML typability is complete for deterministic exponential time. In Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, pages 382–401. ACM SIGACT and SIGPLAN, ACM Press, 1990. [ bib ]
[301] Yu I. Manin. A Course in Mathematical Logic. Springer, New York, 1977. [ bib ]
[302] John Matthews. fCryptol semantics. Available from the author on request, January 2005. [ bib ]
[303] Frank Mayer, Karl MacMillan, and David Caplan. SELinux by Example. Open Source Software Development Series. Prentice Hall, 2007. [ bib ]
[304] David McAllester. Grammar rewriting. In Kapur [511], pages 124–138. [ bib ]
[305] Bill McCarty. SELinux: NSA's Open Source Security Enhanced Linux. O'Reilly, 2005. [ bib ]
[306] Pamela McCorduck. Machines Who Think: A Personal Inquiry into the History and Prospects of Artificial Intelligence. A. K. Peters, March 2004. [ bib ]
[307] Gary McGraw. Software Security: Building Security In. Addison-Wesley Software Security Series. Addison-Wesley, February 2006. [ bib | http ]
[308] Annabelle McIver and Carroll Morgan. Probabilistic predicate transformers: Part 2. Technical Report PRG-TR-5-96, Programming Research Group, Oxford University Computer Laboratory, March 1996. [ bib | .html | Abstract ]
[309] Annabelle McIver, Carroll Morgan, and Elena Troubitsyna. The probabilistic steam boiler: a case study in probabilistic data refinement. In Proceedings of the International Refinement Workshop and Formal Methods Pacific, Canberra, 1998. [ bib | .html | Abstract ]
[310] A. K. McIver and C. Morgan. Demonic, angelic and unbounded probabilistic choices in sequential programs. Acta Informatica, 37(4/5):329–354, 2001. [ bib ]
[311] A. K. McIver and C. C. Morgan. Partial correctness for probabilistic demonic programs. Theoretical Computer Science, 266(1–2):513–541, 2001. [ bib ]
[312] Annabelle McIver and Carroll Morgan. Abstraction, Refinement and Proof for Probabilistic Systems. Springer, 2004. [ bib | http ]
[313] Thomas Frederick Melham. Formalizing Abstraction Mechanisms for Hardware Verification in Higher Order Logic. PhD thesis, University of Cambridge, August 1989. [ bib ]
[314] T. F. Melham. A mechanized theory of the Π-calculus in HOL. Nordic Journal of Computing, 1(1):50–76, 1994. [ bib ]
[315] Jia Meng, Claire Quigley, and Lawrence C. Paulson. Automation for interactive proof: first prototype. Information and Computation, 204(10):1575–1596, 2006. [ bib ]
[316] Gary L. Miller. Riemann's hypothesis and tests for primality. In Conference Record of Seventh Annual ACM Symposium on Theory of Computation, pages 234–239, Albuquerque, New Mexico, May 1975. [ bib ]
[317] Steven P. Miller, Michael W. Whalen, and Darren D. Cofer. Software model checking takes off. Communications of the ACM, 53(2):58–64, February 2010. [ bib | DOI | http ]
[318] R. Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348–375, December 1978. [ bib ]
[319] Robin Milner. Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1989. [ bib ]
[320] Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The Definition of Standard ML. MIT Press, Cambridge, MA, USA, 1997. [ bib ]
[321] J. C. Mogul, R. F. Rashid, and M. J. Accetta. The packet filter: An efficient mechanism for user-level network code. In ACM Symposium on Operating Systems Principles, November 1987. [ bib ]
[322] Abdel Mokkedem and Tim Leonard. Formal verification of the Alpha 21364 network protocol. In Aagaard and Harrison [588], pages 443–461. [ bib ]
[323] David Monniaux. Abstract interpretation of probabilistic semantics. In Seventh International Static Analysis Symposium (SAS'00), number 1824 in Lecture Notes in Computer Science. Springer, 2000. [ bib | .html | Abstract ]
[324] David Monniaux. An abstract Monte-Carlo method for the analysis of probabilistic programs (extended abstract). In 28th Symposium on Principles of Programming Languages (POPL '01). Association for Computer Machinery, 2001. [ bib | .html | Abstract ]
[325] Carroll Morgan, Annabelle McIver, Karen Seidel, and J. W. Sanders. Probabilistic predicate transformers. Technical Report TR-4-95, Oxford University Computing Laboratory Programming Research Group, February 1995. [ bib | .html | Abstract ]
[326] Carroll Morgan. Proof rules for probabilistic loops. In He Jifeng, John Cooke, and Peter Wallis, editors, Proceedings of the BCS-FACS 7th Refinement Workshop, Workshops in Computing. Springer, 1996. [ bib | .html ]
[327] Carroll Morgan, Annabelle McIver, and Karen Seidel. Probabilistic predicate transformers. ACM Transactions on Programming Languages and Systems, 18(3):325–353, May 1996. [ bib ]
[328] Carroll Morgan and Annabelle McIver. pGCL: formal reasoning for random algorithms. South African Computer Journal, 22:14–27, 1999. [ bib | .ps.gz ]
[329] Max Moser, Christopher Lynch, and Joachim Steinbach. Model elimination with basic ordered paramodulation. Available from the authors' web sites, January 1996. [ bib | .ps.gz | Abstract ]
[330] Max Moser, Ortrun Ibens, Reinhold Letz, Joachim Steinbach, Christoph Goller, Johannes Schumann, and Klaus Mayr. SETHEO and E-SETHEO – the CADE-13 systems. Journal of Automated Reasoning, 18:237–246, 1997. [ bib | .ps.gz | Abstract ]
[331] Rajeev Motwani and Prabhakar Raghavan. Randomized Algorithms. Cambridge University Press, Cambridge, England, June 1995. [ bib ]
[332] Kevin P. Murphy, Yair Weiss, and Michael I. Jordan. Loopy belief propagation for approximate inference: An empirical study. In Laskey K.B. and Prade H., editors, Proceedings of the Fifteenth Conference on Uncertainty in Artificial Intelligence, San Francisco, 1999. Morgan Kaufmann. [ bib | .html ]
[333] E. V. Nalimov, G. McC. Haworth, and E. A. Heinz. Space-efficient indexing of chess endgame tables. ICGA Journal, 23(3):148–162, September 2000. [ bib | .ps.gz | Abstract ]
[334] Anthony J. Narkawicz and César Muñoz. Formal verification of air traffic conflict prevention bands algorithms. Technical Report NASA/TM-2010-216706, National Aeronautics and Space Administration, Langley Research Center, Hampton VA 23681-2199, USA, June 2010. [ bib | .pdf ]
[335] George C. Necula and Peter Lee. Proof-carrying code. Technical Report CMU-CS-96-165, Computer Science Department, Carnegie Mellon University, September 1996. [ bib ]
[336] R. P. Nederpel, J. H. Geuvers, and R. C. De Vrijer. Selected Papers on Automath (Studies in Logic and the Foundations of Mathematics: Volume 133). North-Holland, 1994. [ bib ]
[337] Andrzej Nedzusiak. σ-fields and probability. Journal of Formalized Mathematics, 1989. [ bib | .html ]
[338] Andrzej Nedzusiak. Probability. Journal of Formalized Mathematics, 1990. [ bib | .html ]
[339] Greg Nelson and Derek C. Oppen. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems, 1(2):245–257, October 1979. [ bib ]
[340] Greg Nelson and Derek C. Oppen. Fast decision procedures bases on congruence closure. Journal of the Association for Computing Machinery, 27(2):356–364, April 1980. [ bib ]
[341] M. Nesi. Value-passing CCS in HOL. In Joyce and Seger [546], pages 352–365. [ bib ]
[342] Monica Nesi. Formalising Process Calculi in Higher Order Logic. PhD thesis, University of Cambridge, 1986. [ bib | .html ]
[343] Robert Nieuwenhuis and Albert Rubio. Theorem proving with ordering and equality constrained clauses. Journal of Symbolic Computation, 19(4):321–351, April 1995. [ bib ]
[344] R. Nieuwenhuis and A. Rubio. Paramodulation-based theorem proving. In Robinson and Voronkov [402], chapter 7, pages 371–443. [ bib ]
[345] Nils J. Nilsson. Probabilistic logic. Artificial Intelligence, 28(1):71–87, 1986. [ bib ]
[346] Tobias Nipkow. Functional unification of higher-order patterns. In Proceedings, Eighth Annual IEEE Symposium on Logic in Computer Science, pages 64–74. IEEE Computer Society Press, 1993. [ bib | Abstract ]
[347] Tobias Nipkow. Hoare logics in Isabelle/HOL. In H. Schwichtenberg and R. Steinbrüggen, editors, Proof and System-Reliability, pages 341–367. Kluwer, 2002. [ bib | .html ]
[348] Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL—A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. [ bib | http ]
[349] Tobias Nipkow. Social choice theory in HOL. Special Issue of the Journal of Automated Reasoning, 43(3):289–304, October 2009. [ bib | http | Abstract ]
[350] Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL—A Proof Assistant for Higher-Order Logic, October 2011. Available for download at http://isabelle.in.tum.de/dist/Isabelle2011-1/doc/tutorial.pdf. [ bib | .pdf ]
[351] Pilar Nivela and Robert Nieuwenhuis. Saturation of first-order (constrained) clauses with the Saturate system. In Claude Kirchner, editor, Proceedings of the 5th International Conference on Rewriting Techniques and Applications (RTA-93), volume 690 of Lecture Notes in Computer Science, pages 436–440. Springer, June 1993. [ bib ]
[352] Michael Norrish. C formalised in HOL. PhD thesis, University of Cambridge Computer Laboratory, 1998. [ bib ]
[353] Michael Norrish and Konrad Slind. A thread of HOL development. The Computer Journal, 41(1):37–45, 2002. [ bib | Abstract ]
[354] Michael Norrish. Rewriting conversions implemented with continuations. Special Issue of the Journal of Automated Reasoning, 43(3):305–336, October 2009. [ bib | http | Abstract ]
[355] L. Northrup, P. Feiler, R. P. Gabriel, J. Goodenough, R. Linger, T. Longstaff, R. Kazman, M. Klein, D. Schmidt, K. Sullivan, and K. Wallnau. Ultra-Large-Scale Systems: The Software Challenge of the Future. Software Engineering Institute, Carnegie Mellon, 2006. The 2006 report for a 12-month study of ultra-large-scale systems software, sponsored by the United States Department of Defense. [ bib | http ]
[356] John Nunn. Secrets of Rook Endings. Gambit Publications, December 1999. [ bib ]
[357] John Nunn. Secrets of Pawnless Endings. Gambit Publications, expanded edition 2 edition, 2002. [ bib ]
[358] Steven Obua and Sebastian Skalberg. Importing HOL into Isabelle/HOL. In Furbach and Shankar [555], pages 298–302. [ bib | http | Abstract ]
[359] Chris Okasaki. Purely Functional Data Structures. Cambridge University Press, Cambridge, UK, 1998. [ bib | Abstract ]
[360] John O'Leary, Roope Kaivola, and Tom Melham. Relational STE and theorem proving for formal verification of industrial circuit designs. In Jobstmann and Ray [532], pages 97–104. [ bib | .pdf ]
[361] Machigar Ongtang, Stephen McLaughlin, William Enck, and Patrick McDaniel. Semantically rich application-centric security in Android. In ACSAC-2009 [504], pages 340–349. [ bib | .html ]
[362] Sam Owre and Natarajan Shankar. The formal semantics of PVS. Technical Report SRI-CSL-97-2, Computer Science Laboratory, SRI International, Menlo Park, CA, August 1997. [ bib | .html ]
[363] S. Owre, N. Shankar, J. M. Rushby, and D. W. J. Stringer-Calvert. PVS System Guide. Computer Science Laboratory, SRI International, Menlo Park, CA, September 1999. [ bib ]
[364] Sam Owre and N. Shankar. Theory interpretations in PVS. Technical Report SRI-CSL-01-01, SRI International, April 2001. [ bib | .pdf ]
[365] Michael Parks. Number-theoretic test generation for directed rounding. IEEE Transactions on Computers, 49(7):651–658, 2000. [ bib | .pdf | Abstract ]
[366] Christine Paulin, Philippe Audebaud, and Richard Lassaigne. Randomized algorithms in type theory. Slides from a talk delivered at Dagstuhl seminar 01341: Dependent Type Theory meets Practical Programming, August 2001. [ bib | .ps.gz ]
[367] Lawrence C. Paulson. A higher-order implementation of rewriting. Science of Computer Programming, 3:119–149, 1983. [ bib | .pdf | Abstract ]
[368] Lawrence C. Paulson. Set theory for verification: I. From foundations to functions. Journal of Automated Reasoning, 11(3):353–389, 1993. [ bib | .pdf | Abstract ]
[369] Lawrence C. Paulson. Isabelle: A generic theorem prover. Lecture Notes in Computer Science, 828:xvii + 321, 1994. [ bib ]
[370] Lawrence C. Paulson. Set theory for verification: II. Induction and recursion. Journal of Automated Reasoning, 15(2):167–215, 1995. [ bib | .pdf | Abstract ]
[371] Lawrence C. Paulson. Proving properties of security protocols by induction. In CSFW-1997 [510], pages 70–83. [ bib | .ps.gz ]
[372] Lawrence C. Paulson. Mechanizing coinduction and corecursion in higher-order logic. Journal of Logic and Computation, 7(2):175–204, March 1997. [ bib | .ps.gz ]
[373] Lawrence C. Paulson. The Isabelle Reference Manual, October 1998. With contributions by Tobias Nipkow and Markus Wenzel. [ bib ]
[374] Lawrence C. Paulson. Inductive analysis of the Internet protocol TLS. TISSEC, 2(3):332–351, August 1999. [ bib ]
[375] L. C. Paulson. A generic tableau prover and its integration with Isabelle. Journal of Universal Computer Science, 5(3), March 1999. [ bib | http ]
[376] Lawrence C. Paulson. Mechanizing UNITY in Isabelle. ACM Transactions on Computational Logic, 2000. In press. [ bib ]
[377] Lawrence C. Paulson and Kong Woei Susanto. Source-level proof reconstruction for interactive theorem proving. In Schneider and Brandt [598]. [ bib ]
[378] F. Pfenning and C. Schürmann. System description: Twelf — A meta-logical framework for deductive systems. In Ganzinger [515]. [ bib ]
[379] Lee Pike, Mark Shields, and John Matthews. A verifying core for a cryptographic language compiler. In Manolios and Wilding [502], pages 1–10. [ bib | .pdf | Abstract ]
[380] Robert M. Pirsig. Zen and the Art of Motorcycle Maintenance. Morrow, 10th edition, May 1974. [ bib | .html ]
[381] Gordon Plotkin, Colin Stirling, and Mads Tofte, editors. Proof, Language, and Interaction: Essays in Honour of Robin Milner. MIT Press, May 2000. [ bib ]
[382] Andreas Podelski and Andrey Rybalchenko. Transition invariants. In LICS-2004 [558], pages 32–41. [ bib ]
[383] Andreas Podelski and Andrey Rybalchenko. A complete method for the synthesis of linear ranking functions. In Steffen and Levi [606], pages 239–251. [ bib ]
[384] R. Pollack. On extensibility of proof checkers. Lecture Notes in Computer Science, 996:140–161, 1995. [ bib | .ps.gz ]
[385] George Pólya. How to Solve It. Princeton University Press, Princeton, 1948. [ bib ]
[386] Chr. Posthoff and I. S. Herschberg. Computer analysis of a queen endgame. ICCA Journal, 9(4):189–198, 1986. Translation of Komissarchik (1974). [ bib ]
[387] Riccardo Pucella and Jesse A. Tov. Haskell session types with (almost) no class. In Gill [538], pages 25–36. [ bib | Abstract ]
[388] William Pugh. A practical algorithm for exact array dependence analysis. Communications of the ACM, 35(8):102–114, August 1992. [ bib | Abstract ]
[389] K. Quinn. Ever had problems rounding off figures? the stock exchange has. Wall Street Journal, 202(91), November 1983. [ bib | .pdf ]
[390] Florian Rabe. Representing Logics and Logic Translations. PhD thesis, Jacobs University Bremen, May 2008. [ bib | http ]
[391] M. O. Rabin. Probabilistic automata. Information and Control, 6:230–245, 1963. [ bib | Abstract ]
[392] M. O. Rabin. Probabilistic algorithms. In Traub [453], pages 21–39. [ bib ]
[393] Michael O. Rabin. N-process mutual exclusion with bounded waiting by 4log2(N)-valued shared variable. Journal of Computer and System Sciences, 25(1):66–75, August 1982. [ bib ]
[394] Norman Ramsey and Avi Pfeffer. Stochastic lambda calculus and monads of probability distributions. In POPL-2002 [568]. [ bib | .html | Abstract ]
[395] T. S. Ray. An evolutionary approach to synthetic biology, zen and the art of creating life. Artificial Life, 1(1), 1993. [ bib | ftp ]
[396] M. K. Reiter and A. D. Rubin. Anonymous web transactions with crowds. Communications of the ACM, 42(2):32–38, February 1999. [ bib | Abstract ]
[397] Stefan Richter. Formalizing integration theory with an application to probabilistic algorithms. In Slind et al. [594], pages 271–286. [ bib ]
[398] J. A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23–49, January 1965. [ bib ]
[399] J. A. Robinson. Automatic deduction with hyper-resolution. International Journal of Computer Mathematics, 1:227–234, 1965. [ bib ]
[400] J. A. Robinson. A note on mechanizing higher order logic. Machine Intelligence, 5:121–135, 1970. [ bib ]
[401] Abraham Robinson. Non-standard Analysis. Princeton University Press, 1996. [ bib ]
[402] A. Robinson and A. Voronkov, editors. Handbook of Automated Reasoning. Elsevier Science, 2001. [ bib ]
[403] A. J. Roycroft. *C*. EG, 7(119):771, 1996. [ bib ]
[404] A. J. Roycroft. The computer section. EG, 8(123):47–48, 1997. [ bib ]
[405] A. J. Roycroft. *C*. EG, 8(130 Supplement):428, 1998. [ bib ]
[406] A. J. Roycroft. AJRs snippets. EG, 8(131):476, 1999. [ bib ]
[407] Piotr Rudnicki. An overview of the Mizar project. Notes to a talk at the workshop on Types for Proofs and Programs, June 1992. [ bib | .html ]
[408] John Rushby. Formalism in safety cases. In Dale and Anderson [579], pages 3–17. [ bib | http ]
[409] Bertrand Russell. The Autobiography of Bertrand Russell. George Allen & Unwin, London, 1968. 3 volumes. [ bib ]
[410] David M. Russinoff. An experiment with the Boyer-Moore theorem prover: A proof of Wilson's theorem. Journal of Automated Reasoning, 1:121–139, 1985. [ bib ]
[411] Mark Saaltink. Domain checking Z specifications. In C. Michael Holloway and Kelly J. Hayhurst, editors, LFM' 97: Fourth NASA Langley Formal Methods Workshop, pages 185–192, Hampton, VA, September 1997. [ bib | http ]
[412] R. Sattler. Further to the KRP(a2)KbBP(a3) database. ICCA Journal, 11(2/3):82–87, 1988. [ bib ]
[413] J. Schaeffer. One Jump Ahead: Challenging Human Supremacy in Checkers. Springer, New York, 1997. [ bib ]
[414] J. Schaeffer, Y. Bjornsson, N. Burch, R. Lake, P. Lu, and S Sutphen. Building the checkers 10-piece endgame databases. In Herik et al. [521]. [ bib ]
[415] Fred Schneider. Trust in Cyberspace. National Academy Press, 1999. [ bib ]
[416] Bruce Schneier. Applied Cryptography. Wiley, second edition, 1996. [ bib ]
[417] Johann Ph. Schumann. DELTA — A bottom-up processor for top-down theorem provers (system abstract). In Bundy [512]. [ bib | .html ]
[418] Johann Schumann. Tableaux-based theorem provers: Systems and implementations. Journal of Automated Reasoning, 13:409–421, 1994. [ bib | .html | Abstract ]
[419] J. T. Schwartz. Fast probabilistic algorithms for verification of polynomial identities. Journal of the ACM, 27(4):701–717, October 1980. [ bib | .pdf ]
[420] Carl-Johan Seger. Introduction to formal hardware verification. Technical Report TR-92-13, Department of Computer Science, University of British Columbia, June 1992. [ bib | http | Abstract ]
[421] Karen Seidel, Carroll Morgan, and Annabelle McIver. An introduction to probabilistic predicate transformers. Technical Report TR-6-96, Oxford Programming Research Group Technical Report, 1996. [ bib ]
[422] Karen Seidel, Carroll Morgan, and Annabelle McIver. Probabilistic imperative programming: a rigorous approach. In Groves and Reeves [534]. [ bib ]
[423] Natarajan Shankar and Sam Owre. Principles and pragmatics of subtyping in PVS. In D. Bert, C. Choppy, and P. D. Mosses, editors, Recent Trends in Algebraic Development Techniques, WADT '99, volume 1827 of Lecture Notes in Computer Science, pages 37–52, Toulouse, France, September 1999. Springer. [ bib | .html ]
[424] Mark Shields. A language for symmetric-key cryptographic algorithms and its efficient implementation. Available from the author's website, March 2006. [ bib | http | Abstract ]
[425] Jamie Shield, Ian J. Hayes, and David A. Carrington. Using theory interpretation to mechanise the reals in a theorem prover. In Colin Fidge, editor, Electronic Notes in Theoretical Computer Science, volume 42. Elsevier, 2001. [ bib | .html ]
[426] J. H. Silverman. The Arithmetic of Elliptic Curves. Number 106 in Graduate Texts in Mathematics. Springer, 1986. [ bib ]
[427] John Slaney, Arnold Binas, and David Price. Guiding a theorem prover with soft constraints. In de Mántaras and Saitta [524], pages 221–225. [ bib | .pdf | Abstract ]
[428] Konrad Slind. HOL98 Draft User's Manual, Athabasca Release, Version 2, January 1999. Part of the documentation included with the hol98 theorem-prover. [ bib ]
[429] Konrad Slind. Reasoning about Terminating Functional Programs. PhD thesis, Technical University of Munich, 1999. [ bib ]
[430] Konrad Slind and Michael Norrish. The HOL System Tutorial, February 2001. Part of the documentation included with the HOL4 theorem-prover. [ bib | http ]
[431] Konrad Slind and Joe Hurd. Applications of polytypism in theorem proving. In Basin and Wolff [593], pages 103–119. [ bib | http | Abstract ]
[432] R. Solovay and V. Strassen. A fast Monte-Carlo test for primality. SIAM Journal on Computing, 6(1):84–85, March 1977. [ bib ]
[433] Saurabh Srivastava, Michael Hicks, Jeffrey S. Foster, and Patrick Jenkins. Modular information hiding and type-safe linking for C. IEEE Transactions on Software Engineering, 34(3), May/June 2008. [ bib ]
[434] Daryl Stewart. Formal for everyone - Challenges in achievable multicore design and verification. In Cabodi and Singh [531], page 186. [ bib | .pdf ]
[435] L. B. Stiller. Parallel analysis of certain endgames. ICCA Journal, 12(2):55–64, 1989. [ bib ]
[436] Colin Stirling. Bisimulation, model checking and other games, June 1997. Notes for a Mathfit instructional meeting on games and computation, held in Edinburgh, Scotland. [ bib | .ps ]
[437] David Stirzaker. Elementary Probability. Cambridge University Press, 1994. [ bib ]
[438] T. Ströhlein. Untersuchungen über kombinatorische Spiele. PhD thesis, Technical University of Munich, 1970. [ bib ]
[439] Bryan O'Sullivan, John Goerzen, and Don Stewart. Real World Haskell. O'Reilly Media, Inc., 1st edition, 2008. [ bib ]
[440] Christian B. Suttner and Geoff Sutcliffe. The TPTP problem library — v2.1.0. Technical Report JCU-CS-97/8, Department of Computer Science, James Cook University, December 1997. [ bib | .ps.gz ]
[441] Donald Syme. Declarative Theorem Proving for Operational Semantics. PhD thesis, University of Cambridge, 1998. [ bib ]
[442] Donald Syme. A Simplifier/Programmable Grinder for hol98, January 1998. Part of the documentation included with the hol98 theorem-prover. [ bib ]
[443] Tanel Tammet. A resolution theorem prover for intuitionistic logic. In McRobbie and Slaney [513]. [ bib ]
[444] Tanel Tammet. Gandalf version c-1.0c Reference Manual, October 1997. [ bib | http ]
[445] Tanel Tammet. Gandalf. Journal of Automated Reasoning, 18(2):199–204, April 1997. [ bib ]
[446] Tanel Tammet. Towards efficient subsumption. In Kirchner and Kirchner [514]. [ bib ]
[447] J. Tamplin. EGT-query service extending to 6-man pawnless endgame EGTs in DTC, DTM, DTZ and DTZ50 metrics. Available from the web page http://chess.jaet.org/endings/, 2006. [ bib ]
[448] Aaron Tay. A guide to endgames tablebase. Available from the web page http://www.aarontay.per.sg/Winboard/egtb.html, 2006. [ bib ]
[449] Laurent Théry. A quick overview of HOL and PVS, August 1999. Lecture Notes from the Types Summer School '99: Theory and Practice of Formal Proofs, held in Giens, France. [ bib | .html ]
[450] K. Thompson. Retrograde analysis of certain endgames. ICCA Journal, 9(3):131–139, 1986. [ bib ]
[451] Stephen Toulmin. The Uses of Argument. Cambridge University Press, 1958. [ bib ]
[452] David S. Touretzky. Common Lisp: A Gentle Introduction to Symbolic Computation. Benjamin Cummings, 1990. [ bib | .html ]
[453] J. F. Traub, editor. Algorithms and Complexity: New Directions and Recent Results. Academic Press, New York, 1976. [ bib | Abstract ]
[454] A. Trybulec and H. A. Blair. Computer aided reasoning. In Rohit Parikh, editor, Proceedings of the Conference on Logic of Programs, volume 193 of Lecture Notes in Computer Science, pages 406–412, Brooklyn, NY, June 1985. Springer. [ bib ]
[455] Andrzej Trybulec and Howard Blair. Computer assisted reasoning with MIZAR. In Aravind Joshi, editor, Proceedings of the 9th International Joint Conference on Artificial Intelligence, pages 26–28, Los Angeles, CA, August 1985. Morgan Kaufmann. [ bib ]
[456] Alan M. Turing. Checking a large routine. In Report of a Conference on High Speed Automatic Calculating Machines, pages 67–69, Cambridge, England, June 1949. University Mathematical Laboratory. [ bib ]
[457] D. A. Turner. A new implementation technique for applicative languages. Software – Practice and Experience, 9(1):31–49, January 1979. [ bib | Abstract ]
[458] Thomas Tymoczko. The four color problems. Journal of Philosophy, 76, 1979. [ bib ]
[459] Peter Van Roy and Seif Haridi. Concepts, Techniques, and Models of Computer Programming. MIT Press, March 2004. [ bib ]
[460] Moshe Y. Vardi. Why is modal logic so robustly decidable? Technical Report TR97-274, Rice University, April 1997. [ bib | Abstract ]
[461] Norbert Völker. HOL2P - A system of classical higher order logic with second order polymorphism. In Schneider and Brandt [598], pages 334–351. [ bib | http ]
[462] John von Neumann. Various techniques for use in connection with random digits. In von Neumann's Collected Works, volume 5, pages 768–770. Pergamon, 1963. [ bib ]
[463] Tanja E. J. Vos. UNITY in Diversity: A Stratified Approach to the Verification of Distributed Algorithms. PhD thesis, Utrecht University, 2000. [ bib ]
[464] Philip Wadler. The essence of functional programming. In 19th Symposium on Principles of Programming Languages. ACM Press, January 1992. [ bib ]
[465] Philip Wadler. Comprehending monads. Mathematical Structures in Computer Science, 2:461–493, 1992. [ bib | .html | Abstract ]
[466] Stan Wagon. The Banach-Tarski Paradox. Cambridge University Press, 1993. [ bib ]
[467] Keith Wansbrough, Michael Norrish, Peter Sewell, and Andrei Serjantov. Timing UDP: mechanized semantics for sockets, threads and failures. Draft, 2001. [ bib | http ]
[468] Jefferson Hane Weaver. The World of Physics, volume II. Simon and Schuster, New York, 1987. [ bib ]
[469] Morten Welinder. Very efficient conversions. In Schubert et al. [548], pages 340–352. [ bib | http | Abstract ]
[470] Markus Wenzel. Isar - A generic interpretative approach to readable formal proof documents. In Bertot et al. [587], pages 167–184. [ bib ]
[471] Stephen Westfold. Integrating Isabelle/HOL with Specware. In Schneider and Brandt [599]. [ bib ]
[472] Arthur White. Limerick. Mathematical Magazine, 64(2):91, April 1991. [ bib ]
[473] Alfred North Whitehead and Bertrand Russell. Principia Mathematica. Cambridge University Press, Cambridge, 1910. [ bib ]
[474] A. N. Whitehead. An Introduction to Mathematics. Williams and Northgate, London, 1911. [ bib ]
[475] Freek Wiedijk. Mizar light for HOL light. In Boulton and Jackson [590]. [ bib ]
[476] Freek Wiedijk. Mizar's soft type system. In Schneider and Brandt [598], pages 383–399. [ bib ]
[477] David Williams. Probability with Martingales. Cambridge University Press, 1991. [ bib ]
[478] Carl Roger Witty. The Ontic inference language. Master's thesis, MIT, June 1995. [ bib | .html | Abstract ]
[479] Wai Wong. The HOL res_quan library, 1993. HOL88 documentation. [ bib | .html ]
[480] W. Wong. Recording and checking HOL proofs. In Schubert et al. [548], pages 353–368. [ bib | http | Abstract ]
[481] Wai Wong. A proof checker for HOL. Technical Report 389, University of Cambridge Computer Laboratory, March 1996. [ bib ]
[482] Larry Wos, Ross Overbeek, Ewing Lusk, and Jim Boyle. Automated Reasoning: Introduction and Applications. McGraw-Hill, New York, 2nd edition, 1992. [ bib ]
[483] Larry Wos and Gail W. Pieper. A fascinating country in the world of computing: your guide to automated reasoning. World Scientific Publishing Co., Inc., River Edge, NJ, USA, 1999. [ bib | http ]
[484] R. Wu and D. F. Beal. Solving chinese chess endgames by database construction. Information Sciences, 135(3–4):207–228, 2001. [ bib ]
[485] Hongwei Xi. Dependent Types in Practical Programming. PhD thesis, Carnegie Mellon University, September 1998. [ bib | .html ]
[486] Lotfi A. Zadeh. Fuzzy sets. Information and Control, 8:338–353, 1965. [ bib ]
[487] Vincent Zammit. On the Readability of Machine Checkable Formal Proofs. PhD thesis, University of Kent at Canterbury, March 1999. [ bib ]
[488] Lintao Zhang and Sharad Malik. The quest for efficient boolean satisfiability solvers. In Voronkov [517], pages 295–313. [ bib | .pdf ]
[489] Junxing Zhang and Konrad Slind. Verification of Euclid's algorithm for finding multiplicative inverses. In Hurd et al. [597], pages 205–220. [ bib ]
[490] FIPS. Digital Signature Standard. Federal Information Processing Standards Publication 186. U.S. Department of Commerce/NIST National Technical Information Service, May 1994. [ bib | http ]
[491] Galois, Inc. Cryptol Programming Guide, October 2008. Available for download at http://corp.galois.com/storage/files/downloads/Cryptol_ProgrammingGuide.pdf. [ bib | .pdf ]
[492] IEEE. Standard for binary floating-point arithmetic. ANSI/IEEE Standard 754-1985. The Institute of Electrical and Electronic Engineers, Inc., 345 East 47th Street, New York, NY 10017, USA, 1985. [ bib | http ]
[493] IEEE. Standard for Verilog Hardware Description Language. IEEE Standard 1364-2001. The Institute of Electrical and Electronic Engineers, Inc., 345 East 47th Street, New York, NY 10017, USA, 2001. [ bib | Abstract ]
[494] IEEE. Standard for Information Technology—Portable Operating System Interface (POSIX) Base Definitions. IEEE Standard 1003.1-2001. The Institute of Electrical and Electronic Engineers, Inc., 345 East 47th Street, New York, NY 10017, USA, 2001. [ bib | Abstract ]
[495] MoD. Requirements for the Procurement of Safety Critical Software in Defence Equipment. Interim Defence Standard 00-55. Ministry of Defence, Directorate of Standardization, Kentigern House, 65 Brown St, Glasgow G2 8EX, UK, April 1991. [ bib ]
[496] National Security Agency. Fact sheet NSA Suite B cryptography. Published on the web at http://www.nsa.gov/ia/industry/crypto_suite_b.cfm, 2005. [ bib | http ]
[497] National Security Agency. The case for elliptic curve cryptography. Available for download at http://www.nsa.gov/business/programs/elliptic_curve.shtml, January 2009. [ bib | http ]
[498] National Security Agency. NSA Suite B cryptography. Available for download at http://www.nsa.gov/ia/programs/suiteb_cryptography/, November 2010. [ bib | http ]
[499] National Security Agency. Mathematical routines for the NIST prime elliptic curves. Available for download at http://www.nsa.gov/ia/_files/nist-routines.pdf, April 2010. [ bib | .pdf ]
[500] Anonymous. The QED manifesto. In Bundy [512]. [ bib | http ]
[501] H. Jaap Van den Herik and Pieter Spronck, editors. Advances in Computer Games, 12th International Conference (ACG 2009), volume 6048 of Lecture Notes in Computer Science. Springer, May 2010. [ bib | DOI | http ]
[502] Panagiotis Manolios and Matthew Wilding, editors. Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications. HappyJack Books, August 2006. [ bib ]
[503] Proceedings of the 17th Annual Computer Security Applications Conference (ACSAC 2001), 2001. [ bib ]
[504] Proceedings of the 25th Annual Computer Security Applications Conference (ACSAC 2009), December 2009. [ bib ]
[505] Jacques Calmet and Jan Plaza, editors. Artificial Intelligence and Symbolic Computation (AISC '98), volume 1476 of Lecture Notes in Artificial Intelligence, Plattsburgh, New York, USA, September 1998. Springer. [ bib | http ]
[506] Proceedings of the 31st Symposium on Computer Arithmetic (ARITH 2024). IEEE Computer Society, June 2024. [ bib ]
[507] Toby Walsh, editor. Ninth Workshop on Automated Reasoning: Bridging the Gap between Theory and Practice. The Society for the Study of Artificial Intelligence and Simulation of Behaviour, April 2002. [ bib ]
[508] Joost-Pieter Katoen, editor. Formal Methods for Real-Time and Probabilistic Systems, volume 1601 of Lecture Notes in Computer Science, Bamberg, Germany, May 1999. Springer. [ bib | http ]
[509] Gethin Norman, Marta Kwiatkowska, and Dimitar Guelev. AVoCS 2002: Second workshop on automated verification of critical systems. Technical Report CSR-02-6, School of Computer Science, University of Birmingham, April 2002. [ bib ]
[510] 10th Computer Security Foundations Workshop. IEEE Computer Society Press, 1997. [ bib ]
[511] Deepak Kapur, editor. Proceedings of the 11th International Conference on Automated Deduction (CADE-11), volume 607 of Lecture Notes in Artificial Intelligence. Springer, June 1992. [ bib ]
[512] Alan Bundy, editor. 12th International Conference on Automated Deduction (CADE-12), volume 814 of Lecture Notes in Artificial Intelligence. Springer, June 1994. [ bib ]
[513] Michael A. McRobbie and John K. Slaney, editors. 13th International Conference on Automated Deduction (CADE-13), volume 1104 of Lecture Notes in Artificial Intelligence. Springer, July 1996. [ bib ]
[514] Claude Kirchner and Hélène Kirchner, editors. Proceedings of the 15th International Conference on Automated Deduction (CADE-15), volume 1421 of Lecture Notes in Artificial Intelligence. Springer, July 1998. [ bib ]
[515] H. Ganzinger, editor. Proceedings of the 16th International Conference on Automated Deduction (CADE-16), volume 1632 of Lecture Notes in Artificial Intelligence. Springer, July 1999. [ bib ]
[516] David A. McAllester, editor. Proceedings of the 17th International Conference on Automated Deduction (CADE-17), volume 1831 of Lecture Notes in Computer Science. Springer, June 2000. [ bib ]
[517] Andrei Voronkov, editor. Proceedings of the 18th International Conference on Automated Deduction (CADE-18), volume 2392 of Lecture Notes in Artificial Intelligence. Springer, July 2002. [ bib ]
[518] J. L. Fiadeiro et al., editor. CALCO 2005, volume 3629 of Lecture Notes in Computer Science. Springer, 2005. [ bib ]
[519] Thomas Ball and Robert B. Jones, editors. Proceedings of the 18th International Conference on Computer Aided Verification (CAV 2006), volume 4144 of Lecture Notes in Computer Science. Springer, August 2006. [ bib ]
[520] Armin Biere and Roderick Bloem, editors. Proceedings of the 26th International Conference on Computer Aided Verification (CAV 2014), volume 8559 of Lecture Notes in Computer Science. Springer, July 2014. [ bib ]
[521] H. J. van den Herik, H. Iida, and E. A. Heinz, editors. Proceedings of the 10th Advances in Computer Games Conference. Kluwer, November 2003. [ bib ]
[522] Daniel Geist and Enrico Tronci, editors. Correct Hardware Design and Verification Methods (CHARME 2003), volume 2860 of Lecture Notes in Computer Science. Springer, October 2003. [ bib ]
[523] Thierry Coquand, Henri Lombardi, and Marie-Françoise Roy, editors. Mathematics, Algorithms, Proofs, number 05021 in Dagstuhl Seminar Proceedings. Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany, 2006. [ bib ]
[524] Ramon López de Mántaras and Lorenza Saitta, editors. 16th European Conference on Artificial Intelligence (ECAI 2004). IOS Press, August 2004. [ bib ]
[525] D. McGuinness, A. Stump, G. Sutcliffe, and C. Tinelli, editors. Proceedings of the Workshop on Evaluation Methods for Solvers and Quality Metrics for Solutions (EMS+QMS 2010), July 2010. [ bib ]
[526] Christoph Benzmueller, John Harrison, and Carsten Schuermann, editors. Empirically Successful Automated Reasoning in Higher-Order Logic. arXiv.org, December 2005. [ bib | http ]
[527] Proceedings of the EuroSys 2006 Conference, April 2006. [ bib ]
[528] Proceedings of the 7th International Workshop on Formal Aspects of Security & Trust (FAST 2010), September 2010. [ bib ]
[529] Proceedings of Formal Methods 2008, volume 5014 of Lecture Notes in Computer Science. Springer, May 2008. [ bib ]
[530] Mandayam Srivas and Albert Camilleri, editors. Proceedings of the First International Conference on Formal Methods in Computer-Aided Design (FMCAD '96), volume 1166 of Lecture Notes in Computer Science. Springer, 1996. [ bib ]
[531] Gianpiero Cabodi and Satnam Singh, editors. Formal Methods in Computer-Aided Design (FMCAD 2012). IEEE, October 2012. [ bib ]
[532] Barbara Jobstmann and Sandip Ray, editors. Formal Methods in Computer-Aided Design (FMCAD 2013). IEEE, October 2013. [ bib ]
[533] John Fitzgerald, Ian J. Hayes, and Andrzej Tarlecki, editors. Proceedings of Formal Methods Europe 2005, volume 3582 of Lecture Notes in Computer Science. Springer, July 2005. [ bib ]
[534] Lindsay Groves and Steve Reeves, editors. Formal Methods Pacific '97. Springer, July 1997. [ bib | .html ]
[535] Dines Bjørner, Manfred Broy, and Igor V. Pottosin, editors. Proceedings of the International Conference on Formal Methods in Programming and Their Applications, volume 735 of Lecture Notes in Computer Science. Springer, June 1993. [ bib ]
[536] Maria Paola Bonacina and Ulrich Furbach, editors. International Workshop on First-Order Theorem Proving (FTP '97), number 97-50 in RISC-Linz Report Series. Johannes Kepler Universität Linz, October 1997. [ bib | http ]
[537] Ricardo Caferra and Gernot Salzer, editors. International Workshop on First-Order Theorem Proving (FTP '98), Technical Report E1852-GS-981. Technische Universität Wien, November 1998. [ bib | http ]
[538] Andy Gill, editor. Haskell '08: Proceedings of the first ACM SIGPLAN symposium on Haskell. ACM, September 2008. [ bib ]
[539] Chung-chieh Shan, editor. Haskell '13: Proceedings of the 2013 ACM SIGPLAN symposium on Haskell. ACM, September 2013. [ bib ]
[540] High Confidence Software and Systems: HCSS 2006, April 2006. [ bib ]
[541] High Confidence Software and Systems: HCSS 2007, May 2007. [ bib ]
[542] High Confidence Software and Systems: HCSS 2009, May 2009. [ bib ]
[543] John Launchbury and Ray Richards, editors. Proceedings of the Twelfth Annual High Confidence Software and Systems Conference (HCSS 2012), May 2012. [ bib ]
[544] Jan Heering, Karl Meinke, Bernhard Möller, and Tobias Nipkow, editors. Higher-Order Algebra, Logic, and Term Rewriting, First International Workshop (HOA '93), volume 816 of Lecture Notes in Computer Science. Springer, 1994. [ bib ]
[545] Myla Archer, Jeffrey J. Joyce, Karl N. Levitt, and Phillip J. Windley, editors. Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications (HOL '91), August 1991. IEEE Computer Society Press, 1992. [ bib ]
[546] J. J. Joyce and C.-J. H. Seger, editors. Higher Order Logic Theorem Proving and its Applications, 6th International Workshop, volume 780 of Lecture Notes in Computer Science. Springer, August 1993. [ bib ]
[547] Tom Melham and Juanito Camilleri, editors. Higher Order Logic Theorem Proving and Its Applications, 7th International Workshop, volume 859 of Lecture Notes in Computer Science. Springer, September 1994. [ bib ]
[548] E. T. Schubert, P. J. Windley, and J. Alves-Foss, editors. Proceedings of the 8th International Workshop on Higher Order Logic Theorem Proving and Its Applications (HOL '95), volume 971 of Lecture Notes in Computer Science. Springer, September 1995. [ bib ]
[549] Proceedings of the 8th International Workshop on Higher Order Logic Theorem Proving and Its Applications (HOL '95), September 1995. Supplemental proceedings. [ bib ]
[550] F. Orejas, P. G. Spirakis, and J. van Leeuwen, editors. Automata, Languages and Programming, volume 2076 of Lecture Notes in Computer Science. Springer, July 2001. [ bib | http ]
[551] Proceedings of the 3rd IEEE International Conference on Formal Engineering Methods (ICFEM 2000), September 2000. [ bib ]
[552] James Hook and Peter Thiemann, editors. Proceedings of the 13th ACM SIGPLAN international conference on Functional programming (ICFP 2008). ACM, September 2008. [ bib ]
[553] Peter Thiemann and Robby Bruce Findler, editors. Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming (ICFP 2012). ACM, September 2012. [ bib ]
[554] Komei Fukuda, Joris vander Hoeven, Michael Joswig, and Nobuki Takayama, editors. Proceedings of the Third International Congress on Mathematical Software (ICMS 2010), volume 6327 of Lecture Notes in Computer Science. Springer, September 2010. [ bib | http ]
[555] Ulrich Furbach and Natarajan Shankar, editors. Automated Reasoning, Third International Joint Conference (IJCAR 2006), volume 4130 of Lecture Notes in Computer Science. Springer, August 2006. [ bib ]
[556] Lennart Beringer and Amy Felty, editors. Third International Conference on Interactive Theorem Proving (ITP 2012), volume 7406 of Lecture Notes in Computer Science. Springer, August 2012. [ bib ]
[557] Robert S. Boyer, Edward S. Schneider, and Jr. Guy L. Steele, editors. LFP '84: Proceedings of the 1984 ACM Symposium on LISP and functional programming. ACM, August 1984. [ bib ]
[558] 19th IEEE Symposium on Logic in Computer Science (LICS 2004), July 2004. [ bib ]
[559] A. Voronkov, editor. Proceedings of the International Conference on Logic Programming and Automated Reasoning (LPAR '92), volume 624 of Lecture Notes in Artificial Intelligence. Springer, July 1992. [ bib ]
[560] Geoff Sutcliffe and Andrei Voronkov, editors. Logic for Programming, Artificial Intelligence, and Reasoning, 12th International Conference (LPAR 2005), volume 3835 of Lecture Notes in Artificial Intelligence. Springer, December 2005. [ bib ]
[561] Military Communications Conference 2003. IEEE, October 2003. [ bib | http ]
[562] Bernd Wegner. Proceedings of the second North American workshop on mathematical knowledge management (NA-MKM 2004), January 2004. [ bib ]
[563] César Muñoz. Proceedings of the second NASA formal methods symposium (NFM 2010). Technical Report NASA/CP-2010-216215, National Aeronautics and Space Administration, Langley Research Center, Hampton VA 23681-2199, USA, April 2010. [ bib ]
[564] Mihaela Bobaru, Klaus Havelund, Gerard J. Holzmann, and Rajeev Joshi, editors. Third International Symposium on NASA Formal Methods (NFM 2011), volume 6617 of Lecture Notes in Computer Science. Springer, April 2011. [ bib ]
[565] John P. Gallagher and Janis Voigtländer, editors. Proceedings of the ACM SIGPLAN workshop on Partial Evaluation and Program Manipulation (PEPM 2010). ACM, January 2010. [ bib ]
[566] Gabriel Dos Reis and Laurent Théry, editors. PLMMS '09: Proceedings of the ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems. ACM, August 2009. [ bib ]
[567] POPL '78: Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, New York, NY, USA, 1978. ACM. [ bib ]
[568] POPL 2002: The 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, January 2002. [ bib ]
[569] J. Gregory Morrisett and Simon L. Peyton Jones, editors. Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2006). ACM, January 2006. [ bib ]
[570] Jasmin Christian Blanchette and Josef Urban, editors. Proceedings of the Third International Workshop on Proof Exchange for Theorem Proving (PxTP 2013), volume 14 of EPiC Series. EasyChair, June 2013. [ bib ]
[571] A. Cerone and A. Di Pierro, editors. Proceedings of the 2nd Workshop on Quantitative Aspects of Programming Languages (QAPL 2004), volume 112 of Electronic Notes in Theoretical Computer Science (ENTCS). Elsevier, January 2005. [ bib | http ]
[572] Rewriting Techniques and Applications (RTA 2001), volume 2051 of Lecture Notes in Computer Science. Springer, May 2001. [ bib | http ]
[573] Proceedings of the 15th International Conference on the Theory and Applications of Satisfiability Testing (SAT 2012), volume 7317 of Lecture Notes in Computer Science. Springer, June 2012. [ bib ]
[574] Summary of a Workshop on Software Certification and Dependability. The National Academies Press, 2004. [ bib | http | Abstract ]
[575] Marco Bernardo and Alessandro Cimatti, editors. Formal Methods for Hardware Verification, 6th International School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM 2006), volume 3965 of Lecture Notes in Computer Science. Springer, May 2006. [ bib ]
[576] Daniel J. Bernstein and Kris Gaj, editors. Proceedings of the 5th Special-Purpose Hardware for Attacking Cryptographic Systems Workshop (SHARCS 2012), March 2012. [ bib ]
[577] P. Naur and B. Randell, editors. Software Engineering. Scientific Affairs Division, NATO, October 1968. [ bib | http ]
[578] Jeanna Neefe Matthews and Thomas E. Anderson, editors. Proceedings of the 22nd ACM Symposium on Operating Systems Principles. ACM, October 2009. [ bib ]
[579] Chris Dale and Tom Anderson, editors. Making Systems Safer: Proceedings of the Eighteenth Safety-Critical Systems Symposium. Springer, February 2010. [ bib ]
[580] Proceedings of the 3rd International Workshop on Systems Software Verification (SSV 2008), volume 217 of Electronic Notes in Theoretical Computer Science. Elsevier, July 2008. [ bib ]
[581] Myla Archer, Ben Di Vito, and César Muñoz. Design and application of strategies/tactics in higher order logics (strata 2003). Technical Report NASA/CP-2003-212448, NASA, September 2003. [ bib | .pdf ]
[582] Susanne Graf and Michael Schwartzbach, editors. Tools and Algorithms for the Construction and Analysis of Systems: 6th International Conference, TACAS 2000, volume 1785 of Lecture Notes in Computer Science. Springer, March 2000. [ bib ]
[583] Joakim von Wright, Jim Grundy, and John Harrison, editors. Theorem Proving in Higher Order Logics, 9th International Conference, TPHOLs '96, volume 1125 of Lecture Notes in Computer Science. Springer, August 1996. [ bib ]
[584] Elsa L. Gunter and Amy Felty, editors. Theorem Proving in Higher Order Logics, 10th International Conference, TPHOLs '97, volume 1275 of Lecture Notes in Computer Science. Springer, August 1997. [ bib ]
[585] Elsa L. Gunter, editor. Supplemental Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics, TPHOLs '97, August 1997. [ bib ]
[586] Jim Grundy and Malcolm Newey, editors. Theorem Proving in Higher Order Logics, 11th International Conference, TPHOLs '98, volume 1497 of Lecture Notes in Computer Science. Springer, September 1998. [ bib ]
[587] Yves Bertot, Gilles Dowek, André Hirschowitz, Christine Paulin, and Laurent Théry, editors. Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs '99, volume 1690 of Lecture Notes in Computer Science. Springer, September 1999. [ bib | http ]
[588] Mark Aagaard and John Harrison, editors. Theorem Proving in Higher Order Logics, 13th International Conference: TPHOLs 2000, volume 1869 of Lecture Notes in Computer Science. Springer, August 2000. [ bib ]
[589] Mark Aagaard, John Harrison, and Tom Schubert. TPHOLs 2000: Supplemental proceedings. Technical Report CSE-00-009, Oregon Graduate Institute, August 2000. [ bib ]
[590] Richard J. Boulton and Paul B. Jackson, editors. 14th International Conference on Theorem Proving in Higher Order Logics: TPHOLs 2001, volume 2152 of Lecture Notes in Computer Science. Springer, September 2001. [ bib | http ]
[591] Richard J. Boulton and Paul B. Jackson. TPHOLs 2001: Supplemental proceedings. Technical Report EDI-INF-RR-0046, Division of Informatics, University of Edinburgh, September 2001. [ bib | .html ]
[592] Víctor A. Carreño, César A. Muñoz, and Sofiène Tahar, editors. 15th International Conference on Theorem Proving in Higher Order Logics: TPHOLs 2002, volume 2410 of Lecture Notes in Computer Science. Springer, August 2002. [ bib | http ]
[593] David Basin and Burkhart Wolff, editors. 16th International Conference on Theorem Proving in Higher Order Logics: TPHOLs 2003, volume 2758 of Lecture Notes in Computer Science. Springer, September 2003. [ bib | http ]
[594] Konrad Slind, Annette Bunker, and Ganesh Gopalakrishnan, editors. 17th International Conference on Theorem Proving in Higher Order Logics: TPHOLs 2004, volume 3223 of Lecture Notes in Computer Science. Springer, September 2004. [ bib ]
[595] Konrad Slind. TPHOLs 2004: Emerging trends. Technical Report UUCS-04, School of Computing, University of Utah, September 2004. [ bib | http ]
[596] Joe Hurd and Tom Melham, editors. 18th International Conference on Theorem Proving in Higher Order Logics: TPHOLs 2005, volume 3603 of Lecture Notes in Computer Science. Springer, August 2005. [ bib | http ]
[597] Joe Hurd, Edward Smith, and Ashish Darbari. Theorem proving in higher order logics: Emerging trends proceedings. Technical Report PRG-RR-05-02, Oxford University Computing Laboratory, August 2005. [ bib | http ]
[598] Klaus Schneider and Jens Brandt, editors. 20th International Conference on Theorem Proving in Higher Order Logics: TPHOLs 2007, volume 4732 of Lecture Notes in Computer Science. Springer, September 2007. [ bib | http ]
[599] Klaus Schneider and Jens Brandt. Theorem proving in higher order logics: Emerging trends proceedings. Technical Report 364/07, Department of Computer Science, University of Kaiserslautern, August 2007. [ bib | .html ]
[600] César Muñoz Otmane Ait Mohamed and Sofiène Tahar, editors. 21st International Conference on Theorem Proving in Higher Order Logics: TPHOLs 2008, volume 5170 of Lecture Notes in Computer Science. Springer, August 2008. [ bib | http ]
[601] Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors. Theorem Proving in Higher Order Logics, 22nd International Conference (TPHOLs 2009), volume 5674 of Lecture Notes in Computer Science. Springer, August 2009. [ bib ]
[602] R. Matuszewski and A. Zalewska, editors. From Insight to Proof: Festschrift in Honour of Andrzej Trybulec, volume 10(23) of Studies in Logic, Grammar and Rhetoric. University of Bialystok, 2007. [ bib | http ]
[603] Eduardo Giménex and Christine Paulin-Mohring, editors. Types for Proofs and Programs: International Workshop TYPES' 96, volume 1512 of Lecture Notes in Computer Science. Springer, September 1996. [ bib ]
[604] Stefano Berardi, Mario Coppo, and Ferruccio Damiani, editors. Types for Proofs and Programs: Third International Workshop, TYPES 2003, volume 3085 of Lecture Notes in Computer Science. Springer, May 2004. [ bib ]
[605] M. Aderhold, S. Autexier, and H. Mantel, editors. Proceedings of the 6th International Verification Workshop (VERIFY 2010), July 2010. [ bib ]
[606] Bernhard Steffen and Giorgio Levi, editors. Proceedings of the 5th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2004), volume 2937 of Lecture Notes in Computer Science. Springer, January 2004. [ bib ]

This file was generated by bibtex2html 1.99.