| engl. Beschreibung/ Kurzkommentar |
Complexity of modern engineering problems demands use of advanced mathematical models. Costs of development and design of models necessitate early detection of modelling errors, and therefore, require tools for verification of mathematical models. Construction of model verification tools starts with a programming basis, which can be used to formalise the modelling process, and which allows easy transfer into a computer tool to assist the modelling process. A concept for verification of mathematical models based on type theory has been introduced in recent years. The type theory constitutes a formal foundation of modern programming languages, and the use of type theory for modelling purposes supports the idea of easy computer implementation of model verification tools. Thus, the objective of this project is practical implementation of first steps towards computer-supported modelling assistant based on the type-theoretic approach. Moreover, the project will focus on a specific model, which will be discussed and agreed during first meetings. After that, the participants will study how the chosen model can be formalised by help of type theory and will proceed with its computer implementation. Practical realisation of the project can be done in any strongly typed programming languages, such as Haskell, Agda, F# etc.
var sem |
