|
1 % Add your bibtex entries |
|
2 @inproceedings{Aspinall:2007:FIP:1420412.1420429, |
|
3 author = {Aspinall, David and L\"{u}th, Christoph and Winterstein, Daniel}, |
|
4 title = {A Framework for Interactive Proof}, |
|
5 booktitle = {Proceedings of the 14th symposium on Towards Mechanized Mathematical Assistants: 6th International Conference}, |
|
6 series = {Calculemus '07 / MKM '07}, |
|
7 year = {2007}, |
|
8 isbn = {978-3-540-73083-5}, |
|
9 location = {Hagenberg, Austria}, |
|
10 pages = {161--175}, |
|
11 numpages = {15}, |
|
12 url = {http://dx.doi.org/10.1007/978-3-540-73086-6_15}, |
|
13 doi = {http://dx.doi.org/10.1007/978-3-540-73086-6_15}, |
|
14 acmid = {1420429}, |
|
15 publisher = {Springer-Verlag}, |
|
16 address = {Berlin, Heidelberg}, |
|
17 } |
|
18 |
|
19 @Book{armstrong:erlang96, |
|
20 author = {Armstrong, Joe and others}, |
|
21 title = {Concurrent Programming in Erlang}, |
|
22 publisher = {Prentice Hall}, |
|
23 year = {1996} |
|
24 } |
|
25 |
|
26 @TechReport{odersky:scala06, |
|
27 author = {Odersky, Martin and others}, |
|
28 title = {An Overview of the Scala Programming Language}, |
|
29 institution = {\'Ecole Polytechnique F\'ed\'erale de Lausanne (EPFL)}, |
|
30 year = {2006}, |
|
31 type = {Technical Report LAMP-REPORT-2006-001}, |
|
32 address = {1015 Lausanne, Switzerland}, |
|
33 note = {Second Edition}, |
|
34 annote = {http://www.scala-lang.org/sites/default/files/linuxsoft_archives/docu/files/ScalaOverview.pdf} |
|
35 } |
|
36 |
|
37 @article{Haller:2009:SAU:1496391.1496422, |
|
38 author = {Haller, Philipp and Odersky, Martin}, |
|
39 title = {Scala Actors: Unifying thread-based and event-based programming}, |
|
40 journal = {Theor. Comput. Sci.}, |
|
41 volume = {410}, |
|
42 issue = {2-3}, |
|
43 month = {February}, |
|
44 year = {2009}, |
|
45 issn = {0304-3975}, |
|
46 pages = {202--220}, |
|
47 numpages = {19}, |
|
48 url = {http://portal.acm.org/citation.cfm?id=1496391.1496422}, |
|
49 doi = {10.1016/j.tcs.2008.09.019}, |
|
50 acmid = {1496422}, |
|
51 publisher = {Elsevier Science Publishers Ltd.}, |
|
52 address = {Essex, UK}, |
|
53 keywords = {Actors, Concurrent programming, Events, Threads}, |
|
54 } |
|
55 |
|
56 @InProceedings{scala:jmlc06, |
|
57 author = {Philipp Haller and Martin Odersky}, |
|
58 title = {Event-Based Programming without Inversion of Control}, |
|
59 booktitle = {Proc. Joint Modular Languages Conference}, |
|
60 year = 2006, |
|
61 series = {Springer LNCS} |
|
62 } |
|
63 |
|
64 |
|
65 @InProceedings{makarius:isa-scala-jedit, |
|
66 author = {Makarius Wenzel}, |
|
67 title = {Asyncronous Proof Processing with {Isabelle/Scala} and {Isabelle/jEdit}}, |
|
68 booktitle = {User Interfaces for Theorem Provers (UITP 2010)}, |
|
69 year = {2010}, |
|
70 editor = {C. Sacerdoti Coen and D. Aspinall}, |
|
71 address = {Edinburgh, Scotland}, |
|
72 month = {July}, |
|
73 organization = {FLOC 2010 Satellite Workshop}, |
|
74 note = {http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf} |
|
75 } |
|
76 |
|
77 @Book{db:dom-eng, |
|
78 author = {Bj{\o}rner, Dines}, |
|
79 title = {Domain Engineering. Technology Management, Research and Engineering}, |
|
80 publisher = {JAIST Press}, |
|
81 year = {2009}, |
|
82 month = {Feb}, |
|
83 series = {COE Research Monograph Series}, |
|
84 volume = {4}, |
|
85 address = {Nomi, Japan} |
|
86 } |
|
87 |
|
88 @inproceedings{Haftmann-Nipkow:2010:code, |
|
89 author = {Florian Haftmann and Tobias Nipkow}, |
|
90 title = {Code Generation via Higher-Order Rewrite Systems}, |
|
91 booktitle = {Functional and Logic Programming, 10th International |
|
92 Symposium: {FLOPS} 2010}, |
|
93 year = {2010}, |
|
94 publisher = {Springer}, |
|
95 series = {Lecture Notes in Computer Science}, |
|
96 volume = {6009} |
|
97 } |
|
98 |
|
99 @Manual{coq1999, |
|
100 title = {The Coq Proof Assistant}, |
|
101 author = {Barras, B. and others}, |
|
102 organization = {INRIA-Rocquencourt - CNRS-ENS Lyon}, |
|
103 month = {July}, |
|
104 year = {1999}, |
|
105 pnote={},status={cited},source={mkm01.caprotti},location={} |
|
106 } |
|
107 |
|
108 @Book{meta-ML, |
|
109 author = {Gordon,M. and Milner,R. and Wadsworth,C. P.}, |
|
110 title = {Edinburgh LCF: A Mechanised Logic of Computation}, |
|
111 publisher = { Springer-Verlag}, |
|
112 year = {1979}, |
|
113 volume = {78}, |
|
114 series = {Lecture Notes in Computer Science} |
|
115 } |
|
116 |
|
117 @book{Paulson:Isa94, |
|
118 title={Isabelle: a generic theorem prover}, |
|
119 author={Paulson, Lawrence C. }, publisher={Springer-Verlag},year={1994}, |
|
120 volume={828},series={Lecture Notes in Computer Science},address={},edition={},month={}, |
|
121 note={With contributions by Topias Nipkow}, |
|
122 status={},source={},location={-} |
|
123 } |
|
124 |
|
125 @Book{pl:milner97, |
|
126 author = {Robin Milner and Mads Tofte and Robert Harper and David MacQueen}, |
|
127 title = {The Definition of Standard ML (Revised)}, |
|
128 publisher = {The MIT Press}, |
|
129 year = 1997, |
|
130 address = {Cambridge, London}, |
|
131 annote = {97bok375} |
|
132 } |
|
133 |
|
134 @Article{back-grundy-wright-98, |
|
135 author = {Back, Ralph and Grundy, Jim and von Wright, Joakim}, |
|
136 title = {Structured Calculational Proof}, |
|
137 journal = {Formal Aspects of Computing}, |
|
138 year = {1998}, |
|
139 number = {9}, |
|
140 pages = {469-483} |
|
141 } |
|
142 |
|
143 @Manual{isar-impl, |
|
144 title = {The {Isabelle/Isar} Implementation}, |
|
145 author = {Makarius Wenzel}, |
|
146 month = {April 19}, |
|
147 year = {2009}, |
|
148 note = {With contributions by Florian Haftmann and Larry Paulson} |
|
149 } |
|
150 |
|
151 @InProceedings{wenzel:isar, |
|
152 author = {Wenzel, Markus}, |
|
153 title = {Isar - a Generic Interpretative Approach to Readable Formal Proof Documents}, |
|
154 booktitle = {Theorem Proving in Higher Order Logics}, |
|
155 year = {1999}, |
|
156 editor = {G. Dowek, A. Hirschowitz, C. Paulin, L. Thery}, |
|
157 series = {LNCS 1690}, |
|
158 organization = {12th International Conference TPHOLs'99}, |
|
159 publisher = {Springer} |
|
160 } |
|
161 |
|
162 |