neuper@38096
|
1 |
@InProceedings{makarius:isa-scala-jedit,
|
neuper@38096
|
2 |
author = {Makarius Wenzel},
|
neuper@38096
|
3 |
title = {Asyncronous Proof Processing with {Isabelle/Scala} and {Isabelle/jEdit}},
|
neuper@38096
|
4 |
booktitle = {User Interfaces for Theorem Provers (UITP 2010)},
|
neuper@38096
|
5 |
year = {2010},
|
neuper@38096
|
6 |
editor = {C. Sacerdoti Coen and D. Aspinall},
|
neuper@38096
|
7 |
address = {Edinburgh, Scotland},
|
neuper@38096
|
8 |
month = {July},
|
neuper@38096
|
9 |
organization = {FLOC 2010 Satellite Workshop},
|
neuper@38096
|
10 |
note = {http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf}
|
neuper@38096
|
11 |
}
|
neuper@38096
|
12 |
|
neuper@38096
|
13 |
@Book{db:dom-eng,
|
neuper@38096
|
14 |
author = {Bj{\o}rner, Dines},
|
neuper@38096
|
15 |
title = {Domain Engineering. Technology Management, Research and Engineering},
|
neuper@38096
|
16 |
publisher = {JAIST Press},
|
neuper@38096
|
17 |
year = {2009},
|
neuper@38096
|
18 |
month = {Feb},
|
neuper@38096
|
19 |
series = {COE Research Monograph Series},
|
neuper@38096
|
20 |
volume = {4},
|
neuper@38096
|
21 |
address = {Nomi, Japan}
|
neuper@38096
|
22 |
}
|
neuper@38096
|
23 |
|
neuper@38094
|
24 |
@inproceedings{Haftmann-Nipkow:2010:code,
|
neuper@38094
|
25 |
author = {Florian Haftmann and Tobias Nipkow},
|
neuper@38094
|
26 |
title = {Code Generation via Higher-Order Rewrite Systems},
|
neuper@38094
|
27 |
booktitle = {Functional and Logic Programming, 10th International
|
neuper@38094
|
28 |
Symposium: {FLOPS} 2010},
|
neuper@38094
|
29 |
year = {2010},
|
neuper@38094
|
30 |
publisher = {Springer},
|
neuper@38094
|
31 |
series = {Lecture Notes in Computer Science},
|
neuper@38094
|
32 |
volume = {6009}
|
neuper@38094
|
33 |
}
|
neuper@38094
|
34 |
|
neuper@38094
|
35 |
@Manual{coq1999,
|
neuper@38094
|
36 |
title = {The Coq Proof Assistant},
|
neuper@38094
|
37 |
author = {Barras, B. and others},
|
neuper@38094
|
38 |
organization = {INRIA-Rocquencourt - CNRS-ENS Lyon},
|
neuper@38094
|
39 |
month = {July},
|
neuper@38094
|
40 |
year = {1999},
|
neuper@38094
|
41 |
pnote={},status={cited},source={mkm01.caprotti},location={}
|
neuper@38094
|
42 |
}
|
neuper@38094
|
43 |
|
neuper@38094
|
44 |
@Book{meta-ML,
|
neuper@38094
|
45 |
author = {Gordon,M. and Milner,R. and Wadsworth,C. P.},
|
neuper@38094
|
46 |
title = {Edinburgh LCF: A Mechanised Logic of Computation},
|
neuper@38094
|
47 |
publisher = { Springer-Verlag},
|
neuper@38094
|
48 |
year = {1979},
|
neuper@38094
|
49 |
volume = {78},
|
neuper@38094
|
50 |
series = {Lecture Notes in Computer Science}
|
neuper@38094
|
51 |
}
|
neuper@38094
|
52 |
|
neuper@38089
|
53 |
@book{Paulson:Isa94,
|
neuper@38089
|
54 |
title={Isabelle: a generic theorem prover},
|
neuper@38089
|
55 |
author={Paulson, Lawrence C. }, publisher={Springer-Verlag},year={1994},
|
neuper@38089
|
56 |
volume={828},series={Lecture Notes in Computer Science},address={},edition={},month={},
|
neuper@38089
|
57 |
note={With contributions by Topias Nipkow},
|
neuper@38089
|
58 |
status={},source={},location={-}
|
neuper@38089
|
59 |
}
|
neuper@38089
|
60 |
|
neuper@38079
|
61 |
@Book{pl:milner97,
|
neuper@38079
|
62 |
author = {Robin Milner and Mads Tofte and Robert Harper and David MacQueen},
|
neuper@38079
|
63 |
title = {The Definition of Standard ML (Revised)},
|
neuper@38079
|
64 |
publisher = {The MIT Press},
|
neuper@38079
|
65 |
year = 1997,
|
neuper@38079
|
66 |
address = {Cambridge, London},
|
neuper@38079
|
67 |
annote = {97bok375}
|
neuper@38079
|
68 |
}
|
neuper@38079
|
69 |
|
neuper@38079
|
70 |
@Article{back-grundy-wright-98,
|
neuper@38079
|
71 |
author = {Back, Ralph and Grundy, Jim and von Wright, Joakim},
|
neuper@38079
|
72 |
title = {Structured Calculational Proof},
|
neuper@38079
|
73 |
journal = {Formal Aspects of Computing},
|
neuper@38079
|
74 |
year = {1998},
|
neuper@38079
|
75 |
number = {9},
|
neuper@38079
|
76 |
pages = {469-483}
|
neuper@38079
|
77 |
}
|
neuper@38079
|
78 |
|
neuper@38079
|
79 |
@Manual{isar-impl,
|
neuper@38079
|
80 |
title = {The {Isabelle/Isar} Implementation},
|
neuper@38079
|
81 |
author = {Makarius Wenzel},
|
neuper@38079
|
82 |
month = {April 19},
|
neuper@38079
|
83 |
year = {2009},
|
neuper@38079
|
84 |
note = {With contributions by Florian Haftmann and Larry Paulson}
|
neuper@38079
|
85 |
}
|
neuper@38079
|
86 |
|
neuper@38079
|
87 |
@InProceedings{wenzel:isar,
|
neuper@38079
|
88 |
author = {Wenzel, Markus},
|
neuper@38079
|
89 |
title = {Isar - a Generic Interpretative Approach to Readable Formal Proof Documents},
|
neuper@38079
|
90 |
booktitle = {Theorem Proving in Higher Order Logics},
|
neuper@38079
|
91 |
year = {1999},
|
neuper@38079
|
92 |
editor = {G. Dowek, A. Hirschowitz, C. Paulin, L. Thery},
|
neuper@38079
|
93 |
series = {LNCS 1690},
|
neuper@38079
|
94 |
organization = {12th International Conference TPHOLs'99},
|
neuper@38079
|
95 |
publisher = {Springer}
|
neuper@38079
|
96 |
}
|
andreas@38100
|
97 |
|
andreas@38100
|
98 |
|