1.1 --- a/doc-isac/mlehnfeld/master/thesis/introduction.tex	Wed Jul 23 14:09:51 2014 +0200
     1.2 +++ b/doc-isac/mlehnfeld/master/thesis/introduction.tex	Wed Jul 23 14:32:19 2014 +0200
     1.3 @@ -11,9 +11,9 @@
     1.4  \caption{Intel CPU trends (source: \cite{sutter2005free}).}
     1.5  \label{fig:chip-speeds}
     1.6  \end{figure}
     1.7 -Concurrency allows for multitasking and asynchronous computations can improve responsiveness even on uniprocessors (see section \ref{sec:concurresp}). But writing efficiently parallel or concurrent software is hard \cite{sutter2005software}. Now that multi-core architectures are commonplace and higly parallel GPUs are beginning to get exploited for general-purpose computing \cite{nickolls2010gpu}, concurrent processes and threads can effectively be running simultaneously and therefore significantly faster.
     1.8 +Concurrency allows for multitasking and asynchronous computations can improve responsiveness even on uniprocessors (see section \ref{sec:concurresp}). But writing efficiently parallel or concurrent software is hard \cite{sutter2005software}. Now that multi-core architectures are commonplace and highly parallel GPUs are beginning to get exploited for general-purpose computing \cite{nickolls2010gpu}, concurrent processes and threads can effectively be running simultaneously and therefore significantly faster.
     1.9  
    1.10 -Functional programming is a declarative paradigm based on the lambda calculs. It has been claimed that it is specifically suited not only for prototyping but also for efficient parallelism due to some of its defining features such as immutable data, statelessness and the lack of side effects (e.g. \cite{burge1975recursive}).
    1.11 +Functional programming is a declarative paradigm based on the lambda calculus. It has been claimed that it is specifically suited not only for prototyping but also for efficient parallelism due to some of its defining features such as immutable data, statelessness and the lack of side effects (e.g. \cite{burge1975recursive}).
    1.12  
    1.13  The interactive theorem prover \isabelle{} \cite{nipkow2002isabelle} is a comprehensive, international software project. Its internal logic has been written entirely in {\em Standard ML} which later was embedded in a {\em Scala} environment to simplify interaction with the underlying operating system and software built on top of \isabelle{}. As the use of multi-core systems became more common, \isabelle{}'s computationally complex logic was required to exploit the newly available processing power. Makarius Wenzel, one of the leading developers of \isabelle{}, parallelized essential parts of the system within a few man months (scattered over about two years). This is a surprisingly little amount of effort considering the project's size and complexity. A significant amount of the work was required due to the use of impure code, facilitated by \textit{Standard ML} and \textit{Scala}, i.e. work concerning purification in terms of the functional paradigm. {\em Isabelle/Scala} provides tools for interaction between front-end and proof engine and contains object-oriented components to deal with inherently stateful aspects of the development environment {\em Isabelle/jEdit}.
    1.14  
    1.15 @@ -22,4 +22,4 @@
    1.16  
    1.17  \section{Thesis Structure}
    1.18  \label{sec:thesis_structure}
    1.19 -The remainder of this thesis is structured as follows. Chapter \ref{cha:fundamentals} establishes a theoretical background on the different areas relevant for the practical work on the case study within \isac{} and includes topics such as functional programming, computer theorem proving, parallelism, concurrency, responsiveness and refactoring of programs within the functional paradigm. Subsequently, various approaches towards parallelism that can and may have been used in functional programming are investigated in chapter \ref{cha:funproglangs_mcsystems}. The end of this chapter briefly talks about refactoring of functional programs for parallelism. Chapter \ref{cha:isabelle_isac} is then dedicated to the two main software projects involved in the practical part of this thesis, \isabelle{} and \isac{}, as well as to a discussion of what has been done in the course of the practical work. A conclusion and outlook on possible futurework are given in chapter \ref{cha:conclusion}. Appendix \ref{app:code} provides code samples in addition to those given in the main text as well as comments and further explanations. Finally, appendix \ref{app:cdrom} lists the contents of the DVD that was handed in along with the thesis.
    1.20 +The remainder of this thesis is structured as follows. Chapter \ref{cha:fundamentals} establishes a theoretical background on the different areas relevant for the practical work on the case study within \isac{} and includes topics such as functional programming, computer theorem proving, parallelism, concurrency, responsiveness and refactoring of programs within the functional paradigm. Subsequently, various approaches towards parallelism that can and may have been used in functional programming are investigated in chapter \ref{cha:funproglangs_mcsystems}. The end of this chapter briefly talks about refactoring of functional programs for parallelism. Chapter \ref{cha:isabelle_isac} is then dedicated to the two main software projects involved in the practical part of this thesis, \isabelle{} and \isac{}, as well as to a discussion of what has been done in the course of the practical work. A conclusion and outlook on possible future work are given in chapter \ref{cha:conclusion}. Appendix \ref{app:code} provides code samples in addition to those given in the main text as well as comments and further explanations. Finally, appendix \ref{app:cdrom} lists the contents of the DVD that was handed in along with the thesis.