1.1 --- a/doc-src/isac/CTP-userinterfaces.bib Mon Jan 10 10:43:00 2011 +0100
1.2 +++ b/doc-src/isac/CTP-userinterfaces.bib Mon Jan 10 12:36:33 2011 +0100
1.3 @@ -1,3 +1,43 @@
1.4 +@inproceedings{Haftmann-Nipkow:2010:code,
1.5 + author = {Florian Haftmann and Tobias Nipkow},
1.6 + title = {Code Generation via Higher-Order Rewrite Systems},
1.7 + booktitle = {Functional and Logic Programming, 10th International
1.8 +Symposium: {FLOPS} 2010},
1.9 + year = {2010},
1.10 + publisher = {Springer},
1.11 + series = {Lecture Notes in Computer Science},
1.12 + volume = {6009}
1.13 +}
1.14 +
1.15 +@InProceedings{wenzel:isar,
1.16 + author = {Wenzel, Markus},
1.17 + title = {Isar - a Generic Interpretative Approach to Readable Formal Proof Documents},
1.18 + booktitle = {Theorem Proving in Higher Order Logics},
1.19 + year = {1999},
1.20 + editor = {G. Dowek, A. Hirschowitz, C. Paulin, L. Thery},
1.21 + series = {LNCS 1690},
1.22 + organization = {12th International Conference TPHOLs'99},
1.23 + publisher = {Springer}
1.24 +}
1.25 +
1.26 +@Manual{coq1999,
1.27 + title = {The Coq Proof Assistant},
1.28 + author = {Barras, B. and others},
1.29 + organization = {INRIA-Rocquencourt - CNRS-ENS Lyon},
1.30 + month = {July},
1.31 + year = {1999},
1.32 + pnote={},status={cited},source={mkm01.caprotti},location={}
1.33 +}
1.34 +
1.35 +@Book{meta-ML,
1.36 + author = {Gordon,M. and Milner,R. and Wadsworth,C. P.},
1.37 + title = {Edinburgh LCF: A Mechanised Logic of Computation},
1.38 + publisher = { Springer-Verlag},
1.39 + year = {1979},
1.40 + volume = {78},
1.41 + series = {Lecture Notes in Computer Science}
1.42 +}
1.43 +
1.44 @book{Paulson:Isa94,
1.45 title={Isabelle: a generic theorem prover},
1.46 author={Paulson, Lawrence C. }, publisher={Springer-Verlag},year={1994},