1.1 --- a/doc-src/isac/CTP-userinterfaces.bib	Tue Jan 11 12:34:29 2011 +0100
     1.2 +++ b/doc-src/isac/CTP-userinterfaces.bib	Tue Jan 11 13:39:39 2011 +0100
     1.3 @@ -1,8 +1,8 @@
     1.4 -@TechReport{,
     1.5 +@TechReport{odersky:scala06,
     1.6    author = 	 {Odersky, Martin, et.al.},
     1.7    title = 	 {An Overview of the Scala Programming Language},
     1.8    institution =  {\'Ecole Polytechnique F\'ed\'erale de Lausanne (EPFL)},
     1.9 -  year = 	 {},
    1.10 +  year = 	 {2006},
    1.11    type = 	 {Technical Report LAMP-REPORT-2006-001},
    1.12    address = 	 {1015 Lausanne, Switzerland},
    1.13    note = 	 {Second Edition},

     2.1 --- a/doc-src/isac/CTP-userinterfaces.tex	Tue Jan 11 12:34:29 2011 +0100
     2.2 +++ b/doc-src/isac/CTP-userinterfaces.tex	Tue Jan 11 13:39:39 2011 +0100
     2.3 @@ -20,9 +20,11 @@
     2.4  \begin{document}
     2.5  \maketitle
     2.6  \abstract{
     2.7 +This paper accompanies a pre-study on a sub-project planned within the \sisac-project. The goal of this sub-project is to extend ther userinterface of the theorem prover Isabelle such, that Structured Derivations according to R.J.Back are interactively processed. The sub-project is one step towards using the upcoming Isabelle/Isar/Scala layer for /sisac.
     2.8  
     2.9 +The paper comprises three parts: (1) Ample space is given to background information about the state of the art in user interfaces for theorem provers and about the upcoming requirements for future developments. (2) focuses the strategy of Isabelle, the motivations and first decision. (3) provides a protocol of preparatory work for the sub-project. 
    2.10  
    2.11 -}
    2.12 +By the way, this paper shall serve as an entry point for students interested in joining the \sisac-team.}
    2.13  
    2.14  \section{Introduction}\label{intro}
    2.15  Computer Theorem Provers (CTPs \footnote{The term CTP is used to address two different things in this paper: (1) the academic discipline comprising respective theories as well as (2) the products developed within this discipline, the provers and the respective technology.}) have a tradition as long as Computer Algebra Systems (CAS), another kind of mathematics assistants. However, CTPs task of proving is more challenging than calculating; so, in contrary to CASs, CTPs are not yet in widespread use --- not yet, because CTPs are on the step into industrial use in the current decade: Safe-critical software requires to be proven correct more and more \cite{db:dom-eng}, and the technology of CTP becomes ready to accomplish the task of efficiently proving hundreds of proof obligations.
    2.16 @@ -172,7 +174,7 @@
    2.17  Proof scripts are  sequences of commands however proof documents are  structured texts. 
    2.18  So the proof document idea seems to guarantee the perfect support for parallelism in the CTP technology. 
    2.19  (MW async-isabelle-scala.pdf)
    2.20 -\newpage
    2.21 +
    2.22  %Andreas
    2.23  \section{Isabelle's plans for new user-interfaces}\label{gui-plans}
    2.24  %       http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf,\\
    2.25 @@ -431,7 +433,20 @@
    2.26  \end{enumerate}
    2.27  As the example above illustrates, a conversion of Scala- to Java-objects is possible. It looks easy but also a little bit useless. Why should you need this? Just imagine that there is a Plugin written in Scala and one coded in Java. With this connection between Scala and Java, it would be easy to connect this two Plugins! 
    2.28  %Diesen direkten Zusammenhang zwischen Java und Scala soll anhand der Grafik-Bibliotheken Swing. Beide Sprachen stellen diese Grafik-Bibliotheken zur Verfügung (und darin auch eigene Shapes und Funktionalität). Es ist jedoch möglich, Java-Bibliotheken, wie eben auch Java-Swing in Scala zu verwenden. Ein JButton kann zum Beispiel mittels \textit{import javax.swing.JButton} eingebunden und damit sofort auch verwendet werden. Auch Scala stellt in seiner Swing-Bibliothek zur Verfügung: \textit{scala.swing.Button}. Es wird nahezu die selbe Funktionalität angeboten und teilweise die Erzeugung bzw. Verwendung vereinfacht(???). Man kann sich nun fragen, warum sich die Scala-Entwickler einerseit die Mühe gemacht haben die Verwendung Java-Swing, wie in Java selbst, möglich zu machen und andererseits mit Scala-Swing eine nahezu idente Alternative geschaffen haben. Die Antwort darauf zeigt wie der objektorientierte Teil von Scala in vielen Bereichen aufgebaut wurden. Es wurde kein neues Konzept für diese Grafikklassen entworfen sondern Wrapper-Objekte/Methoden/Klassen erstellt, die das Arbeiten mit diesen Grafikkomponenten erleichtern soll. Ein Letztes Problem bleibt noch: Es ist zwar sehr einfach ein Java-Swing-Objekt an einen Scala-Swing-Container (zb. Frame) anzubinden, da eine Konvertierung von Java-Komponente in ein Scala-Äquivalent ist problemlos möglich. ...
    2.29 +
    2.30  \section{Conclusion and future work}
    2.31 +This paper collected background information on the topic of userinterfaces for theorem provers, which is not covered by the standard curriculum at Graz University of Technology: Computer theorem proving, respective interfaces and novel challenges for userinterfaces raised by integration of CTP into software engineering tools within the current decade.
    2.32 +
    2.33 +The general background informations has been related to students' knowledge already gained during studies: functional and object-oriented programming paradigm, programming languages with focus on Scala and Scala's specific concept to handle asyncronous processing of proof documents, the concept of actors.
    2.34 +
    2.35 +An important part of the paper is a protocol of preparatory work already done on project-setup and software components required for the next goal: extend the theorem prover Isabelle with Structured Derivations.
    2.36 +
    2.37 +This part is considered an appropriate to start realising this goal preparing future work, which will join the \sisac-project with front-of-the-wave technology in computer theorem proving and respective userinterfaces.
    2.38 +
    2.39 +\bigskip textbf{Acknowledgements}\\
    2.40 +The authors thank the lecturer of 'Verfassen wissenschaftlicher Arbeiten' in winter semester 2010/11, Dipl.-Ing. Dr.techn. Markus Strohmaier, for his support on working on the topic they are interested in.\\
    2.41 +The leader of the \sisac-project expresses his pleasure about the efficient collaboration between the institutes IICM and IST at TUG.
    2.42 +
    2.43  
    2.44  
    2.45  \bibliography{CTP-userinterfaces}