Von TTTT zu Liqud Haskell
Liquid Haskell (LH) ist ein Refinement Type System, das auf Haskell aufbaut, um die funktionale Korrektheit des Codes zu gewährleisten. Dies wird durch die Verfeinerung der Haskell-Typen mit logischen Prädikaten erreicht, mit denen sich wichtige Eigenschaften zur Kompilierzeit durchsetzen lassen [1]. In LH geschriebene Funktionen müssen terminierend sein, was zur Kompilierzeit verifiziert wird, wobei derzeit Quasi-Befehle verwendet werden, die auf Erweiterungen von Term-Rewrite-Systemen (TRS) erster Ordnung angewendet werden. Wir nutzen die Möglichkeit, statische Terminierungsprüfer für TRSs, wie das Tyrolean Termination Tool (TTTT), nach dem Stand der Technik zu integrieren.
Betreuer_in
Georg Moser
Domänenspezifische maschinelle Übersetzung für TeX-Dateien
Maschinelle Übersetzungssysteme haben inzwischen ein bemerkenswertes Leistungsniveau erreicht und den Übersetzungsprozess in mehreren Sprachen erheblich erleichtert. Trotz dieser Fortschritte gibt es jedoch noch Defizite bei der Anpassung an spezielle Formate wie z. B. TeX-Dateien, die in der akademischen Welt weit verbreitet sind. In dieser Arbeit soll diese Lücke durch die Entwicklung eines maschinellen Übersetzungssystems, das speziell für die Übersetzung von TeX-Dateien konzipiert ist, zu schließen. Darüber hinaus zielt die Arbeit auf domänenspezifische Optimierungen ab, die auf computerwissenschaftliche Inhalte zugeschnitten sind. Die größte Herausforderung besteht darin, die komplexe Struktur des Dokuments während der Übersetzung beizubehalten und gleichzeitig die Verwendung einer angemessenen Terminologie zu gewährleisten.
Betreuer_in
Samuel Frontull
Automatisierte Ableitung von linguistischen Klanggesetzen
In dieser Arbeit wird ein neuer Ansatz zur automatisierten Inferenz linguistischer Klangesetze und zur phonetischen Modellierung entwickelt, der auf aktuellen Methoden und Modellen aus der Sequenzanalyse, der historischen Computerlinguistik und der Bioinformatik basiert. Der aktuelle Stand der Technik wird erörtert und die Methoden werden mit dem neuen Ansatz in Bezug auf verschiedene Metriken wie Leistung, Genauigkeit und Nutzen verglichen.
Betreuer_in
Samuel Frontull, Georg Moser
Automatische Ressourcen und Terminationsanalyse von Logischen Programmen
Im Rahmen dieses Projekts soll ein leichtgewichtiger Ressourcen- und Terminierungsanalysator für logische Programme (unter Einbeziehung einer signifikanten Teilmenge von Prolog) als eigenständiges Werkzeug implementiert oder in TcT integriert werden. Der Prover sollte in der Lage sein, Lehrbuchbeispiele in Prolog zu bearbeiten.
Student_in
Morgan Couapel
Betreuer_in
Georg Moser
CLARA: Automatisiertes Feedback für Programmieraufgaben
Manuelles Feedback zu Programmieraufgaben ist (i) mühsam, (ii) zeitaufwendig und (iii) fehleranfällig. Die Bachelorarbeit (für den Lehramtsabschluss) untersucht neuere Arbeiten zur automatischen Bereitstellung von Feedback. Das von Gulwani et al. entwickelte Werkzeug CLARA nutzt Methoden der Programmreparatur, um die kleinste Reparatur als Feedback zu liefern. In dieser Arbeit wird der Prototyp für kleine Programmieraufgaben, wie sie typischerweise in Lehrveranstaltungen an der Universität Innsbruck vorkommen, experimentell validiert.
Student_in
Natalie Höpperger
Betreuer_in
Georg Moser
Umsetzungen des 'Bring Your Own Device' an österreichischen Schulen
Die Arbeit wird Fragen rund um die Geräteoffensive 'Digitales Lernen' beantworten und findet unter der Mitwirkung von Mag. Rene Braunshier (BRG/BORG Landeck) statt.
Student_in
Jonas Pfurtscheller
Betreuer_in
Georg Moser
Effiziente Programme lernen
Was ist der Stand der Technik auf dem Gebiet der induktiven Programmierung, wenn es um komplexe, effiziente, rekursive Programme geht? Ist es z.B. gewährleistet, dass anspruchsvolle Lehrbuchbeispiele mit wenigen Beispielen erlernt werden können? Hier interessiert uns vor allem die Effizienz von Programmen. Ziel der Bachelorarbeit ist es, einen vertieften Überblick über bestehende Methoden der induktiven Programmierung zu geben, unabhängig vom zugrunde liegenden Programmierparadigma. Dazu werden Literaturstudien, theoretische, sowie experimentelle Vergleiche durchgeführt.
Student_in
Natalie Höpperger
Betreuer_in
Georg Moser