|
1 @inproceedings{Haftmann-Nipkow:2010:code, |
|
2 author = {Florian Haftmann and Tobias Nipkow}, |
|
3 title = {Code Generation via Higher-Order Rewrite Systems}, |
|
4 booktitle = {Functional and Logic Programming, 10th International |
|
5 Symposium: {FLOPS} 2010}, |
|
6 year = {2010}, |
|
7 publisher = {Springer}, |
|
8 series = {Lecture Notes in Computer Science}, |
|
9 volume = {6009} |
|
10 } |
|
11 |
|
12 @InProceedings{wenzel:isar, |
|
13 author = {Wenzel, Markus}, |
|
14 title = {Isar - a Generic Interpretative Approach to Readable Formal Proof Documents}, |
|
15 booktitle = {Theorem Proving in Higher Order Logics}, |
|
16 year = {1999}, |
|
17 editor = {G. Dowek, A. Hirschowitz, C. Paulin, L. Thery}, |
|
18 series = {LNCS 1690}, |
|
19 organization = {12th International Conference TPHOLs'99}, |
|
20 publisher = {Springer} |
|
21 } |
|
22 |
|
23 @Manual{coq1999, |
|
24 title = {The Coq Proof Assistant}, |
|
25 author = {Barras, B. and others}, |
|
26 organization = {INRIA-Rocquencourt - CNRS-ENS Lyon}, |
|
27 month = {July}, |
|
28 year = {1999}, |
|
29 pnote={},status={cited},source={mkm01.caprotti},location={} |
|
30 } |
|
31 |
|
32 @Book{meta-ML, |
|
33 author = {Gordon,M. and Milner,R. and Wadsworth,C. P.}, |
|
34 title = {Edinburgh LCF: A Mechanised Logic of Computation}, |
|
35 publisher = { Springer-Verlag}, |
|
36 year = {1979}, |
|
37 volume = {78}, |
|
38 series = {Lecture Notes in Computer Science} |
|
39 } |
|
40 |
1 @book{Paulson:Isa94, |
41 @book{Paulson:Isa94, |
2 title={Isabelle: a generic theorem prover}, |
42 title={Isabelle: a generic theorem prover}, |
3 author={Paulson, Lawrence C. }, publisher={Springer-Verlag},year={1994}, |
43 author={Paulson, Lawrence C. }, publisher={Springer-Verlag},year={1994}, |
4 volume={828},series={Lecture Notes in Computer Science},address={},edition={},month={}, |
44 volume={828},series={Lecture Notes in Computer Science},address={},edition={},month={}, |
5 note={With contributions by Topias Nipkow}, |
45 note={With contributions by Topias Nipkow}, |