neuper@38096: @InProceedings{makarius:isa-scala-jedit, neuper@38096: author = {Makarius Wenzel}, neuper@38096: title = {Asyncronous Proof Processing with {Isabelle/Scala} and {Isabelle/jEdit}}, neuper@38096: booktitle = {User Interfaces for Theorem Provers (UITP 2010)}, neuper@38096: year = {2010}, neuper@38096: editor = {C. Sacerdoti Coen and D. Aspinall}, neuper@38096: address = {Edinburgh, Scotland}, neuper@38096: month = {July}, neuper@38096: organization = {FLOC 2010 Satellite Workshop}, neuper@38096: note = {http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf} neuper@38096: } neuper@38096: neuper@38096: @Book{db:dom-eng, neuper@38096: author = {Bj{\o}rner, Dines}, neuper@38096: title = {Domain Engineering. Technology Management, Research and Engineering}, neuper@38096: publisher = {JAIST Press}, neuper@38096: year = {2009}, neuper@38096: month = {Feb}, neuper@38096: series = {COE Research Monograph Series}, neuper@38096: volume = {4}, neuper@38096: address = {Nomi, Japan} neuper@38096: } neuper@38096: neuper@38094: @inproceedings{Haftmann-Nipkow:2010:code, neuper@38094: author = {Florian Haftmann and Tobias Nipkow}, neuper@38094: title = {Code Generation via Higher-Order Rewrite Systems}, neuper@38094: booktitle = {Functional and Logic Programming, 10th International neuper@38094: Symposium: {FLOPS} 2010}, neuper@38094: year = {2010}, neuper@38094: publisher = {Springer}, neuper@38094: series = {Lecture Notes in Computer Science}, neuper@38094: volume = {6009} neuper@38094: } neuper@38094: neuper@38094: @Manual{coq1999, neuper@38094: title = {The Coq Proof Assistant}, neuper@38094: author = {Barras, B. and others}, neuper@38094: organization = {INRIA-Rocquencourt - CNRS-ENS Lyon}, neuper@38094: month = {July}, neuper@38094: year = {1999}, neuper@38094: pnote={},status={cited},source={mkm01.caprotti},location={} neuper@38094: } neuper@38094: neuper@38094: @Book{meta-ML, neuper@38094: author = {Gordon,M. and Milner,R. and Wadsworth,C. P.}, neuper@38094: title = {Edinburgh LCF: A Mechanised Logic of Computation}, neuper@38094: publisher = { Springer-Verlag}, neuper@38094: year = {1979}, neuper@38094: volume = {78}, neuper@38094: series = {Lecture Notes in Computer Science} neuper@38094: } neuper@38094: neuper@38089: @book{Paulson:Isa94, neuper@38089: title={Isabelle: a generic theorem prover}, neuper@38089: author={Paulson, Lawrence C. }, publisher={Springer-Verlag},year={1994}, neuper@38089: volume={828},series={Lecture Notes in Computer Science},address={},edition={},month={}, neuper@38089: note={With contributions by Topias Nipkow}, neuper@38089: status={},source={},location={-} neuper@38089: } neuper@38089: neuper@38079: @Book{pl:milner97, neuper@38079: author = {Robin Milner and Mads Tofte and Robert Harper and David MacQueen}, neuper@38079: title = {The Definition of Standard ML (Revised)}, neuper@38079: publisher = {The MIT Press}, neuper@38079: year = 1997, neuper@38079: address = {Cambridge, London}, neuper@38079: annote = {97bok375} neuper@38079: } neuper@38079: neuper@38079: @Article{back-grundy-wright-98, neuper@38079: author = {Back, Ralph and Grundy, Jim and von Wright, Joakim}, neuper@38079: title = {Structured Calculational Proof}, neuper@38079: journal = {Formal Aspects of Computing}, neuper@38079: year = {1998}, neuper@38079: number = {9}, neuper@38079: pages = {469-483} neuper@38079: } neuper@38079: neuper@38079: @Manual{isar-impl, neuper@38079: title = {The {Isabelle/Isar} Implementation}, neuper@38079: author = {Makarius Wenzel}, neuper@38079: month = {April 19}, neuper@38079: year = {2009}, neuper@38079: note = {With contributions by Florian Haftmann and Larry Paulson} neuper@38079: } neuper@38079: neuper@38079: @InProceedings{wenzel:isar, neuper@38079: author = {Wenzel, Markus}, neuper@38079: title = {Isar - a Generic Interpretative Approach to Readable Formal Proof Documents}, neuper@38079: booktitle = {Theorem Proving in Higher Order Logics}, neuper@38079: year = {1999}, neuper@38079: editor = {G. Dowek, A. Hirschowitz, C. Paulin, L. Thery}, neuper@38079: series = {LNCS 1690}, neuper@38079: organization = {12th International Conference TPHOLs'99}, neuper@38079: publisher = {Springer} neuper@38079: } andreas@38100: andreas@38100: