| 39307 |      1 | 
 | 
|  |      2 | @string{LNCS="Lecture Notes in Computer Science"}
 | 
|  |      3 | @string{Springer="Springer-Verlag"}
 | 
|  |      4 | 
 | 
|  |      5 | @inproceedings{Bulwahn-et-al:2008:imp_HOL,
 | 
|  |      6 |   author =      {Lukas Bulwahn and Alexander Krauss and Florian Haftmann and Levent Erk{\"o}k and John Matthews},
 | 
|  |      7 |   title =       {Imperative Functional Programming with {Isabelle/HOL}},
 | 
|  |      8 |   booktitle =   {TPHOLs '08: Proceedings of the 21th International Conference on Theorem Proving in Higher Order Logics},
 | 
|  |      9 |   year =        {2008},
 | 
|  |     10 |   isbn =        {978-3-540-71065-3},
 | 
|  |     11 |   pages =       {352--367},
 | 
|  |     12 |   publisher =   Springer,
 | 
|  |     13 |   series =      LNCS,
 | 
|  |     14 |   volume =      {5170},
 | 
|  |     15 |   editor =      {Otmane A\"{\i}t Mohamed and C{\'e}sar Mu{\~n}oz and Sofi{\`e}ne Tahar}
 | 
|  |     16 | }
 | 
|  |     17 | 
 | 
|  |     18 | @book{Nipkow-et-al:2002:tutorial,
 | 
|  |     19 |   author =      {T. Nipkow and L. C. Paulson and M. Wenzel},
 | 
|  |     20 |   title =       {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},
 | 
|  |     21 |   series =      LNCS,
 | 
|  |     22 |   volume =      2283,
 | 
|  |     23 |   year =        2002,
 | 
|  |     24 |   publisher =   Springer
 | 
|  |     25 | }
 |