138 volume = {4573}, |
138 volume = {4573}, |
139 year = {2007}, |
139 year = {2007}, |
140 isbn = {978-3-540-73083-5}, |
140 isbn = {978-3-540-73083-5}, |
141 bibsource = {DBLP, http://dblp.uni-trier.de} |
141 bibsource = {DBLP, http://dblp.uni-trier.de} |
142 } |
142 } |
|
143 |
|
144 @InProceedings{gdaroczy-EP-13, |
|
145 author = {Gabriella Dar\'{o}czy and Walther Neuper}, |
|
146 title = {Exploitation of ``Next-Step-Guidance'' in a {TP}-based Math Assistant}, |
|
147 OPTpages = {TODO-TODO}, |
|
148 crossref = {eduTPS-12} |
|
149 } |
|
150 |
|
151 |
|
152 @Proceedings{eduTPS-12, |
|
153 title = {Theorem-Prover based Systems for Education (eduTPS)}, |
|
154 year = {2013}, |
|
155 OPTkey = {}, |
|
156 OPTbooktitle = {}, |
|
157 OPTeditor = {}, |
|
158 OPTvolume = {}, |
|
159 OPTnumber = {}, |
|
160 OPTseries = {}, |
|
161 OPTaddress = {}, |
|
162 OPTmonth = {}, |
|
163 OPTorganization = {}, |
|
164 publisher = {The Electronic Journal of Mathematics and Technology}, |
|
165 note = {to appear}, |
|
166 OPTannote = {} |
|
167 } |
|
168 |
|
169 @Misc{nipkow-prog-prove, |
|
170 author = {Nipkow, Tobias}, |
|
171 title = {Programming and Proving in {Isabelle/HOL}}, |
|
172 howpublished = {contained in the Isabelle distribution}, |
|
173 month = {May 22}, |
|
174 year = {2012} |
|
175 } |
|
176 |
|
177 @Book{pl:hind97, |
|
178 author = {J. Roger Hindley}, |
|
179 title = {Basic Simple Type Theory}, |
|
180 publisher = {Cambridge University Press}, |
|
181 year = 1997, |
|
182 editor = {S. Abramsky and P. H. Aczel and others}, |
|
183 number = 42, |
|
184 series = {Cambridge Tracts in Theoretical Computer Science}, |
|
185 address = {Cambridge}, |
|
186 annote = {97bok308} |
|
187 } |
|
188 |
|
189 @Article{Milner-78, |
|
190 author = {Milner, R.}, |
|
191 title = {A Theory of Type Polymorphism in Programming}, |
|
192 journal = {Journal of Computer and System Science (JCSS)}, |
|
193 year = {1978}, |
|
194 number = {17}, |
|
195 pages = {348-374} |
|
196 } |