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