doc-isac/mlehnfeld/master/thesis/abstract.tex
author wneuper <Walther.Neuper@jku.at>
Sun, 31 Dec 2023 09:42:27 +0100
changeset 60787 26037efefd61
parent 55466 55c2d2ee3f92
permissions -rw-r--r--
Doc/Specify_Phase 2: copy finished
     1 \chapter{Abstract}
     2 \label{cha:abstract}
     3 
     4 Multi-core hardware has become a standard in personal computing. Similar to the {\em software crisis} around 1970, writing software which is able to exploit the new, parallel hardware is still a difficult, error-prone process.
     5 
     6 Due to a side effect free programming style, functional programming languages are said to be specifically suitable for this kind of tasks. One application of such languages are theorem provers. Their foundation in mathematics and logics makes functional programming the paradigm of choice. {\em Isabelle} is an interactive theorem proving framework whose back-end has been implemented in {\em Standard ML}. Development efforts during recent years have enabled the system to efficiently use the full processing power available on current multi-core architectures. The educational mathematics system \isac{} draws on {\em Isabelle}'s functionality and was thus until recently the only project of its kind to be based on theorem proving technology.
     7 
     8 This thesis documents the introduction of {\em Isabelle}'s parallelism concepts to \isac{} and outlines related technologies such as parallelism fundamentals, various approaches to parallelism in functional programming and computer theorem proving. Furthermore, the architectures and concepts of {\em Isabelle} and \isac{} are discussed, both including means of communicating with the {\em Java Virtual Machine} for their front-ends. Thereby the strengths of functional and imperative programming are combined and both paradigms are utilized to solve the respective problems for which they are particularly appropriate. The results of the parallelization are promising and will enable a high number of students to use one single, responsive \isac{} server for calculations simultaneously.