@inproceedings{Haftmann-Nipkow:2010:code,

  author =      {Florian Haftmann and Tobias Nipkow},

  title =       {Code Generation via Higher-Order Rewrite Systems},

  booktitle =   {Functional and Logic Programming, 10th International

Symposium: {FLOPS} 2010},

  year =        {2010},

  publisher =   {Springer},

  series =      {Lecture Notes in Computer Science},

  volume =      {6009}

}

@InProceedings{wenzel:isar,

  author = 	 {Wenzel, Markus},

  title = 	 {Isar - a Generic Interpretative Approach to Readable Formal Proof Documents},

  booktitle = 	 {Theorem Proving in Higher Order Logics},

  year = 	 {1999},

  editor = 	 {G. Dowek, A. Hirschowitz, C. Paulin, L. Thery},

  series = 	 {LNCS 1690},

  organization = {12th International Conference TPHOLs'99},

  publisher = {Springer}

}

@Manual{coq1999,

  title = 	 {The Coq Proof Assistant},

  author = 	 {Barras, B. and others},

  organization = {INRIA-Rocquencourt - CNRS-ENS Lyon},

  month = 	 {July},

  year = 	 {1999},

  pnote={},status={cited},source={mkm01.caprotti},location={}  

}

@Book{meta-ML,

  author = 	 {Gordon,M. and Milner,R.  and Wadsworth,C. P.},

  title = 	 {Edinburgh LCF: A Mechanised Logic of Computation},

  publisher = 	 { Springer-Verlag},

  year = 	 {1979},

  volume = 	 {78},

  series = 	 {Lecture Notes in Computer Science}

}

@book{Paulson:Isa94,

        title={Isabelle: a generic theorem prover}, 

        author={Paulson, Lawrence C. }, publisher={Springer-Verlag},year={1994}, 

	volume={828},series={Lecture Notes in Computer Science},address={},edition={},month={}, 

	note={With contributions by Topias Nipkow},

        status={},source={},location={-} 

        }  

@Book{pl:milner97,

  author = 	 {Robin Milner and Mads Tofte and Robert Harper and David MacQueen},

  title = 	 {The Definition of Standard ML (Revised)},

  publisher = 	 {The MIT Press},

  year = 	 1997,

  address =	 {Cambridge, London},

  annote =	 {97bok375}

}

@Article{back-grundy-wright-98,

  author = 	 {Back, Ralph and Grundy, Jim and von Wright, Joakim},

  title = 	 {Structured Calculational Proof},

  journal = 	 {Formal Aspects of Computing},

  year = 	 {1998},

  number = 	 {9},

  pages = 	 {469-483}

}

@Manual{isar-impl,

  title = 	 {The {Isabelle/Isar} Implementation},

  author = 	 {Makarius Wenzel},

  month = 	 {April 19},

  year = 	 {2009},

  note = 	 {With contributions by Florian Haftmann and Larry Paulson}

}

@InProceedings{wenzel:isar,

  author = 	 {Wenzel, Markus},

  title = 	 {Isar - a Generic Interpretative Approach to Readable Formal Proof Documents},

  booktitle = 	 {Theorem Proving in Higher Order Logics},

  year = 	 {1999},

  editor = 	 {G. Dowek, A. Hirschowitz, C. Paulin, L. Thery},

  series = 	 {LNCS 1690},

  organization = {12th International Conference TPHOLs'99},

  publisher = {Springer}

}