doc-src/manual.bib
changeset 6619 010dfaf75064
parent 6613 250a0ca35ef5
child 6624 e0914e542f00
equal deleted inserted replaced
6618:13293a7d4a57 6619:010dfaf75064
   545   organization	= {Computer Science Laboratory, SRI International},
   545   organization	= {Computer Science Laboratory, SRI International},
   546   address	= {Menlo Park, CA},
   546   address	= {Menlo Park, CA},
   547   note		= {Beta release},
   547   note		= {Beta release},
   548   year		= 1993,
   548   year		= 1993,
   549   month		= apr,
   549   month		= apr,
   550   url		= {\verb|http://www.csl.sri.com/reports/pvs-language.dvi.Z|}}
   550   url		= {\url{http://www.csl.sri.com/reports/pvs-language.dvi.Z}}}
   551 
   551 
   552 %P
   552 %P
   553 
   553 
   554 % replaces paulin92
   554 % replaces paulin92
   555 @InProceedings{paulin-tlca,
   555 @InProceedings{paulin-tlca,
   570   author	= {Lawrence C. Paulson},
   570   author	= {Lawrence C. Paulson},
   571   title		= {A Formulation of the Simple Theory of Types (for
   571   title		= {A Formulation of the Simple Theory of Types (for
   572 		 {Isabelle})}, 
   572 		 {Isabelle})}, 
   573   pages		= {246-274},
   573   pages		= {246-274},
   574   crossref	= {colog88},
   574   crossref	= {colog88},
   575   url		= {http://www.cl.cam.ac.uk/Research/Reports/TR175-lcp-simple.dvi.gz}}
   575   url		= {\url{http://www.cl.cam.ac.uk/Research/Reports/TR175-lcp-simple.dvi.gz}}}
   576 
   576 
   577 @Article{paulson-coind,
   577 @Article{paulson-coind,
   578   author	= {Lawrence C. Paulson},
   578   author	= {Lawrence C. Paulson},
   579   title		= {Mechanizing Coinduction and Corecursion in Higher-Order
   579   title		= {Mechanizing Coinduction and Corecursion in Higher-Order
   580 		  Logic},
   580 		  Logic},
   601   journal	= JAR,
   601   journal	= JAR,
   602   volume	= 5,
   602   volume	= 5,
   603   number	= 3,
   603   number	= 3,
   604   pages		= {363-397},
   604   pages		= {363-397},
   605   year		= 1989,
   605   year		= 1989,
   606   url		= {http://www.cl.cam.ac.uk/Research/Reports/TR130-lcp-generic-theorem-prover.dvi.gz}}
   606   url		= {\url{http://www.cl.cam.ac.uk/Research/Reports/TR130-lcp-generic-theorem-prover.dvi.gz}}}
   607 
   607 
   608 %replaces paulson-final
   608 %replaces paulson-final
   609 @Article{paulson-mscs,
   609 @Article{paulson-mscs,
   610   author	= {Lawrence C. Paulson},
   610   author	= {Lawrence C. Paulson},
   611   title		= {Final Coalgebras as Greatest Fixed Points in ZF Set Theory},
   611   title		= {Final Coalgebras as Greatest Fixed Points in ZF Set Theory},
   668   title		= {Natural Deduction as Higher-order Resolution},
   668   title		= {Natural Deduction as Higher-order Resolution},
   669   journal	= JLP,
   669   journal	= JLP,
   670   volume	= 3,
   670   volume	= 3,
   671   pages		= {237-258},
   671   pages		= {237-258},
   672   year		= 1986,
   672   year		= 1986,
   673   url		= {http://www.cl.cam.ac.uk/Research/Reports/TR82-lcp-higher-order-resolution.dvi.gz}}
   673   url		= {\url{http://www.cl.cam.ac.uk/Research/Reports/TR82-lcp-higher-order-resolution.dvi.gz}}}
   674 
   674 
   675 @Article{paulson-set-I,
   675 @Article{paulson-set-I,
   676   author	= {Lawrence C. Paulson},
   676   author	= {Lawrence C. Paulson},
   677   title		= {Set Theory for Verification: {I}.  {From}
   677   title		= {Set Theory for Verification: {I}.  {From}
   678 		 Foundations to Functions},
   678 		 Foundations to Functions},
   690   journal	= JAR,
   690   journal	= JAR,
   691   volume	= 15,
   691   volume	= 15,
   692   number	= 2,
   692   number	= 2,
   693   pages		= {167-215},
   693   pages		= {167-215},
   694   year		= 1995,
   694   year		= 1995,
   695   url		= {http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz}}
   695   url		= {\url{http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz}}}
   696 
   696 
   697 @article{paulson85,
   697 @article{paulson85,
   698   author	= {Lawrence C. Paulson},
   698   author	= {Lawrence C. Paulson},
   699   title		= {Verifying the Unification Algorithm in {LCF}},
   699   title		= {Verifying the Unification Algorithm in {LCF}},
   700   journal	= SCP,
   700   journal	= SCP,
   713 @incollection{paulson700,
   713 @incollection{paulson700,
   714   author	= {Lawrence C. Paulson},
   714   author	= {Lawrence C. Paulson},
   715   title		= {{Isabelle}: The Next 700 Theorem Provers},
   715   title		= {{Isabelle}: The Next 700 Theorem Provers},
   716   crossref	= {odifreddi90},
   716   crossref	= {odifreddi90},
   717   pages		= {361-386},
   717   pages		= {361-386},
   718   url		= {http://www.cl.cam.ac.uk/Research/Reports/TR143-lcp-experience.dvi.gz}}
   718   url		= {\url{http://www.cl.cam.ac.uk/Research/Reports/TR143-lcp-experience.dvi.gz}}}
   719 
   719 
   720 % replaces paulson-ns and paulson-security
   720 % replaces paulson-ns and paulson-security
   721 @Article{paulson-jcs,
   721 @Article{paulson-jcs,
   722   author	= {Lawrence C. Paulson},
   722   author	= {Lawrence C. Paulson},
   723   title		= {The Inductive Approach to Verifying Cryptographic Protocols},
   723   title		= {The Inductive Approach to Verifying Cryptographic Protocols},
   774 		  Experiment},
   774 		  Experiment},
   775   institution	= {Computer Laboratory, University of Cambridge},
   775   institution	= {Computer Laboratory, University of Cambridge},
   776   year		= 1995,
   776   year		= 1995,
   777   number	= 364,
   777   number	= 364,
   778   month		= may,
   778   month		= may,
   779   url		= {http://www.cl.cam.ac.uk:80/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz}}
   779   url		= {\url{http://www.cl.cam.ac.uk:80/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz}}}
   780 
   780 
   781 @Book{reeves90,
   781 @Book{reeves90,
   782   author	= {Steve Reeves and Michael Clarke},
   782   author	= {Steve Reeves and Michael Clarke},
   783   title		= {Logic for Computer Science},
   783   title		= {Logic for Computer Science},
   784   publisher	= {Addison-Wesley},
   784   publisher	= {Addison-Wesley},