src/HOL/ex/document/root.bib
changeset 15871 e524119dbf19
parent 14569 78b75a9eec01
child 33026 8f35633c4922
equal deleted inserted replaced
15870:4320bce5873f 15871:e524119dbf19
       
     1 
       
     2 
     1 
     3 
     2 @TechReport{Gordon:1985:HOL,
     4 @TechReport{Gordon:1985:HOL,
     3   author =       {M. J. C. Gordon},
     5   author =       {M. J. C. Gordon},
     4   title =        {{HOL}: A machine oriented formulation of higher order logic},
     6   title =        {{HOL}: A machine oriented formulation of higher order logic},
     5   institution =  {University of Cambridge Computer Laboratory},
     7   institution =  {University of Cambridge Computer Laboratory},
   103   author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
   105   author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
   104   title		= {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
   106   title		= {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
   105   publisher	= {Springer},
   107   publisher	= {Springer},
   106   year		= 2002,
   108   year		= 2002,
   107   note		= {LNCS 2283}}
   109   note		= {LNCS 2283}}
       
   110 
       
   111 @Misc{McMillan-LectureNotes,
       
   112   author =	 {Ken McMillan},
       
   113   title =	 {Lecture notes on verification of digital and hybrid systems},
       
   114   note =	 {{NATO} summer school, \url{http://www-cad.eecs.berkeley.edu/~kenmcmil/tutorial/toc.html}}
       
   115 }
       
   116 
       
   117 @PhdThesis{McMillan-PhDThesis,
       
   118   author = 	 {Ken McMillan},
       
   119   title = 	 {Symbolic Model Checking: an approach to the state explosion problem},
       
   120   school = 	 {Carnegie Mellon University},
       
   121   year = 	 1992
       
   122 }