TTTT goes Liquid Haskell
Liquid Haskell (LH) is a refinement type system build on top of Haskell to ensure functional correctness of its code. This is achieved by refining Haskell's types with logical predicates that let you enforce important properties at compile time [1]. Functions written in LH need to be terminating, which is verified during compile-time, currently using well quasi orders employed on extensions of first-order term rewrite systems (TRSs). We exploit the possibility to integrate state-of-the-arte static termination checkers for TRSs, like the Tyrolean Termination Tool (TTTT).
Supervisor
Georg Moser
Domain-Specific Machine Translation for TeX Files
Machine translation (MT) systems have reached a remarkable level of accuracy and have greatly facilitated the translation process in several languages. However, despite these advances, there are still shortcomings in adapting to specialised formats such as TeX files, which are widely used in academia. This thesis aims to close this gap by developing a machine translation system specifically designed for the translation of TeX files. Furthermore, the work aims at domain-specific optimisations tailored to computer science content. The main challenge is to maintain the complex structure of the document during translation while ensuring the use of appropriate terminology.
Supervisor
Samuel Frontull
Automated Derivation of Linguistic Sound Laws
In this thesis, a new approach to automated inference of linguistic sound laws and phonetic modelling is developed based on current methods and models from sequence analysis, historical computational linguistics, and bioinformatics. The current state of the art is discussed and its methods are compared with the new approach in terms of various metrics, such as performance, accuracy, and usefulness.
Supervisor
Samuel Frontull, Georg Moser
Automated Resource and Termination Analysis of Logic Programs
Within this project a lightweight resource and termination analyser for logic programs (incorporating a significant subset of Prolog) is to be implemented as stand-alone tool or to be incorporated into TcT. The prover should be able to hande textbook examples in Prolog.
Student
Morgan Couapel
Supervisor
Georg Moser
CLARA: Automated Feedback for Programming Assignments
Manually provided feedback to programming assignments is (i) tedious, (ii) time consuming and (iii) error-prone. The bachelor thesis (for the teaching degree) studies recent work to provide feedback automatically. The tool CLARA, developed by Gulwani et al. exploits methods from program repair to provide the smallest repair as feedback. In this thesis, we experimentally validate the prototype for small-scale programming assignments as we typically see in courses at the University of Innsbruck
Student
Natalie Höpperger
Supervisor
Georg Moser
Implementation of 'Bring Your Own Device' at Austrian schools
The work will answer questions relating to the 'Digital Learning' device offensive and will take place with the participation of Rene Braunshier (BRG/BORG Landeck).
Student
Jonas Pfurtscheller
Supervisor
Georg Moser
Learning Efficient Programs
What is the state-of-the-art in the field of inductive programming when it comes to complex, efficient, recursive programs. Is it eg. guranteed that sophisticated text-book examples can be learnt by a few examples? Here, we are particular interested in the efficiency of programs. The aim of the bachelor project is to provide an indepth overview over existing methods in inductive programming independent of the underlying programming paradigmn. For that literature study, theoretical, as well as experimental comparions will be performed.
Student
Natalie Höpperger
Supervisor
Georg Moser