neuper@38114: @inproceedings{Aspinall:2007:FIP:1420412.1420429, neuper@38114: author = {Aspinall, David and L\"{u}th, Christoph and Winterstein, Daniel}, neuper@38114: title = {A Framework for Interactive Proof}, neuper@38114: booktitle = {Proceedings of the 14th symposium on Towards Mechanized Mathematical Assistants: 6th International Conference}, neuper@38114: series = {Calculemus '07 / MKM '07}, neuper@38114: year = {2007}, neuper@38114: isbn = {978-3-540-73083-5}, neuper@38114: location = {Hagenberg, Austria}, neuper@38114: pages = {161--175}, neuper@38114: numpages = {15}, neuper@38114: url = {http://dx.doi.org/10.1007/978-3-540-73086-6_15}, neuper@38114: doi = {http://dx.doi.org/10.1007/978-3-540-73086-6_15}, neuper@38114: acmid = {1420429}, neuper@38114: publisher = {Springer-Verlag}, neuper@38114: address = {Berlin, Heidelberg}, neuper@38114: } neuper@38114: andreas@38113: @Book{armstrong:erlang96, neuper@38114: author = {Armstrong, Joe and others}, andreas@38102: title = {Concurrent Programming in Erlang}, andreas@38102: publisher = {Prentice Hall}, andreas@38102: year = {1996} andreas@38102: } andreas@38102: neuper@38110: @TechReport{odersky:scala06, neuper@38114: author = {Odersky, Martin and others}, neuper@38097: title = {An Overview of the Scala Programming Language}, neuper@38097: institution = {\'Ecole Polytechnique F\'ed\'erale de Lausanne (EPFL)}, neuper@38110: year = {2006}, neuper@38097: type = {Technical Report LAMP-REPORT-2006-001}, neuper@38097: address = {1015 Lausanne, Switzerland}, neuper@38097: note = {Second Edition}, neuper@38097: annote = {http://www.scala-lang.org/sites/default/files/linuxsoft_archives/docu/files/ScalaOverview.pdf} neuper@38097: } neuper@38097: neuper@38097: @article{Haller:2009:SAU:1496391.1496422, neuper@38097: author = {Haller, Philipp and Odersky, Martin}, neuper@38097: title = {Scala Actors: Unifying thread-based and event-based programming}, neuper@38097: journal = {Theor. Comput. Sci.}, neuper@38097: volume = {410}, neuper@38097: issue = {2-3}, neuper@38097: month = {February}, neuper@38097: year = {2009}, neuper@38097: issn = {0304-3975}, neuper@38097: pages = {202--220}, neuper@38097: numpages = {19}, neuper@38097: url = {http://portal.acm.org/citation.cfm?id=1496391.1496422}, neuper@38097: doi = {10.1016/j.tcs.2008.09.019}, neuper@38097: acmid = {1496422}, neuper@38097: publisher = {Elsevier Science Publishers Ltd.}, neuper@38097: address = {Essex, UK}, neuper@38097: keywords = {Actors, Concurrent programming, Events, Threads}, neuper@38097: } neuper@38097: neuper@38097: @InProceedings{scala:jmlc06, neuper@38097: author = {Philipp Haller and Martin Odersky}, neuper@38097: title = {Event-Based Programming without Inversion of Control}, neuper@38097: booktitle = {Proc. Joint Modular Languages Conference}, neuper@38097: year = 2006, neuper@38097: series = {Springer LNCS} neuper@38097: } neuper@38097: neuper@38097: 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: