Die folgenden Themenvorschläge sind unvollständig und naturgemäß oft nicht ganz aktuell! Weitere Themen auch aus anderen Gebieten sind möglich. Kontaktieren Sie bei Interesse daher auf jeden Fall Michael Hanus bzw. die jeweils ausgeführte Kontaktperson.
Von: Michael Hanus
Viele Implementierungen von Programmiersprachen, insbesondere funktionale, logische und auch Skriptsprachen, stellen eine REPL (Read Eval Print Loop) zur Verfügung, womit man einfach Programme interaktiv ausführen kann. Wie der Name schon sagt, liest die REPL einen Ausdruck ein, führt diesen aus und gibt die berechneten Ergebnisse aus, bevor dann der nächste Ausdruck eingelesen wird. Die Entwicklung einer REPL zusätzlich zu einem Compiler macht oft viel zusätzliche Arbeit. Daher könnte man, wenn man einen Compiler mit einer genau definierten Schnittstelle (Aufrufparameter) zur Verfügung hat, die REPL unabhängig vom Compiler implementieren, indem die REPL als separates Programm entwickelt wird, die einen Ausdruck einliest und zur Auswertung daraus ein Hauptprogramm generiert, welches dann mit dem Compiler übersetzt und zum Ablauf gebracht wird. Dies wird tatsächlich in einigen Compilern so gemacht. In dieser Arbeit soll mit dieser Idee eine universelle REPL realisiert werden, die dann durch eine einfache Konfiguration für verschiedene Curry-Compiler (z.B. [1], [2] und neuere in der Entwicklung befindliche Compiler) genutzt werden kann.
Beinhaltet:
Eignung: Bachelorarbeit
Von: Michael Hanus
Berechnungen in deklarativen Programmiersprachen basieren in der Regel auf einer Termgraphstruktur, d.h. Terme mit Sharing von (Variablen-)Knoten. Neuere Implementierungen von logisch-funktionalen Programmiersprachen stellen den gesamten Berechnungszustand in Form von Graphen dar, wodurch optimale und vollständige Berechnungsstrategien unterstützt werden. In einem kürzlich erschienen Artikel wird eine Zwischensprache, genannt ICurry, zur Übersetzung von Curry in imperative Sprachen wie C, Java, Python, Go, u.ä. vorgeschlagen. ICurry basiert auf einfachen Operationen zur Graphmanipulation. Hierzu existiert mit dem Paket icurry [1] auch ein einfacher Interpreter für ICurry, dessen Berechnungen mit Hilfe von graphviz visualisiert werden können. Die Visualisierung ist allerdings sehr einfach und nicht auf Termgraphen zugeschnitten, sodass diese nur für sehr kleine Berechnungen brauchbar ist. Aus diesem Grund soll in dieser Arbeit eine geeignete Visualisierung realisiert werden, mit der man auch größere Berechnungen in einem Web-Browser anzeigen lassen und zwischen verschiedenen Darstellungen (text/graphbasiert) wechseln kann.
Eignung: Bachelorarbeit
[1] https://www-ps.informatik.uni-kiel.de/~cpm/pkgs/icurry.html
[2] http://graphviz.org/
Von: Michael Hanus
Ein wesentlicher Unterschied zwischen den Programmiersprachen Haskell und Curry ist die Pattern-Matching-Strategie. Während in Haskell die Pattern in einer Regel von links nach rechts getestet werden und nur die jeweils erste passende Regel verwendet wird, verwendet Curry eine optimale Strategie mit nichtdeterministischer Selektion aller passenden Regeln. Für rein funktionale Berechnungen sind Haskell-Definitionen manchmal kürzer als in Curry. Außerdem können Haskell-Programme auf Grund dieser Unterschiede nicht direkt als Curry-Programme ausgeführt werden. Daher soll in dieser Arbeit eine Quellsprachentransformation entwickelt werden, die z.B. in den Curry-Präprozessor [1] eingebaut oder auch als separates Tool bereitgestellt wird, mit dessen Hilfe man Curry-Programme mit der Semantik von Haskell ausführen kann. Hierzu können z.B. Funktionen, bei denen dieser Unterschied relevant ist, in case-Ausdrücke übersetzt werden. Eine andere Möglichkeit ist die Übersetzung mit Default-Regeln [2], wodurch es möglich wird, auch logisch-orientierte Berechnungen durchzuführen. Die Transformation soll daher über entsprechende Parameter steuerbar sein.
Eignung: Bachelorarbeit
[1] https://www-ps.informatik.uni-kiel.de/~cpm/pkgs/currypp.html
[2] http://doi.org/10.1017/S1471068416000168
von: Sandra
Da die Arbeit mit JavaScript oftmals mit Kopfschmerzen und Fluchen verbunden ist, soll eine Anbindung an eine existierende JavaScript-Bibliothek (jsCoq [1]) durch eine funktionale JavaScript-Alternative implementiert werden. Dabei stehen Elm, PureScript und Reason als Alternativen zur Auswahl. Je nach Vorlieben des Studierenden kann hier der Fokus auf den Vergleich zwischen den Alternativen gesetzt werden oder auf die Entwicklung eines interaktiven Tutorials.
Eignung: Bachelorarbeit
[1] https://github.com/jscoq/jscoq
[2] https://elm-lang.org
[3] https://www.purescript.org
[4] https://reasonml.github.io
von: Sandra
Beinhaltet:
Bei der Modellierung von Haskell-Programmen in Coq [1] tritt das Problem auf, dass durch die Transformationen der Datenstrukturen, Coq nicht mehr in der Lage ist, ein Induktionsprinzip zu generieren, das stark genug ist, um Beweise zu führen. Solche Induktionsprinzipien generiert der Beweisassistent Coq [2] automatisch; der Nutzen kann aber auch selbstdefinierte Funktionen für die Beweisführung mittels Induktion zur Verfügung stellen. Im Rahmen dieser Bachelorarbeit sollen mithilfe der Coq-Bibliothek elpi zur Metaprogrammierung [3], Induktionsprinzipien automatisch generiert werden, die derzeit manuell definiert werden müssen.
Eignung: Bachelorarbeit
[1] https://github.com/FreeProving/free-proving-code
[2] https://softwarefoundations.cis.upenn.edu/lf-current/IndPrinciples.html
[3] https://github.com/LPCIC/coq-elpi
von: Sandra
Beinhaltet:
Für den Beweisassistenten Coq [1] exisitiert eine Bibliothek zur Programmierung mittels Pattern Matching [2] wie es aus Haskell bekannt ist. Im Rahmen dieser Bachelorarbeit sollen bestehende Modellierungen und Beweise von Aussagen über Haskell-Programme [3] mithilfe dieser Bibliothek portiert werden. Die Kernfrage ist dabei, ob die Verwendung der Bibliothek technische Vorteile bietet, als auch eine Erleichterung der Beweisführung für den Nutzer mit sich bringt.
Eignung: Bachelorarbeit
[1] https://softwarefoundations.cis.upenn.edu/lf-current/toc.html
[2] https://github.com/mattam82/Coq-Equations
[3] https://github.com/FreeProving/free-proving-code
Beinhaltet:
Im Zuge der Implementierung einer Bibliothek zur Modellierung von algebraischen Effekten sind handschriftliche Beweise über Monadenstrukturen entstanden, die im Rahmen dieser Bachelorarbeit mit dem Beweisassistenten Coq [1] formalisiert werden sollen. Viele Beweisschritte sind dabei schon dokumentiert, dennoch ist der Adaptierung von handschriftlichen Beweisen nicht immer 1-zu-1 möglich, so dass der Studierende hier neben der Einarbeitung in Coq auch Eigenleistung bei der Beweisführung zeigen muss.
Eignung: Bachelorarbeit
[1] https://softwarefoundations.cis.upenn.edu/lf-current/toc.html
Beinhaltet:
Basierend auf einer aktueller Entwicklung einer Bibliothek zur Modellierung von algebraischen Effekten in Haskell soll eine bestehende Implementierung zur probabilistischen Programmierung in Curry [1] portiert werden. Algebraische Effekte [2] werden dabei als Alternative zur monadischen Implementierung verwendet. Probabilistische Programmierung kombiniert Nichtdeterminismus mit Wahrscheinlichkeiten.
Eignung: Bachelorarbeit
[1] https://github.com/finnteegen/pflp
[2] https://github.com/fused-effects/fused-effects
Von: Finn
Nachdem Curry kürzlich um Typ- und Typkonstruktorklassen erweitert wurde, soll in einem nächsten Schritt die Unterstützung für Multiparametertypklassen hinzugefügt werden. Um dabei möglicherweise auftretende Mehrdeutigkeiten aufzulösen, soll es weiterhin möglich sein, wie in Haskell funktionale Abhängigkeiten zwischen den Typklassenparametern spezifizieren zu können. Beides kann durch entsprechende Anpassungen im gemeinsamen Front-End von KiCS2 und PAKCS erreicht werden.
Beinhaltet:
Eignung: Masterarbeit
[1] https://www.informatik.uni-kiel.de/~mh/lehre/abschlussarbeiten/msc/Teegen.pdf
[2] http://web.cecs.pdx.edu/~mpj/pubs/fundeps-esop2000.pdf
Von: Michael
SMT-Löser können verwendet werden, um bestimmte Programmeigenschaften automatisch zu beweisen. Dies wurde z.B. durchgeführt, um Verträge statisch zu prüfen oder automatisch zu beweisen, dass Programme fehlerfrei sind, d.h. nicht abstürzen. Hierzu werden bestimmte Eigenschaften aus Quellprogrammen extrahiert und in SMT-Skripte übersetzt. Falls diese Eigenschaften nicht bewiesen werden können, können SMT-Löser auch Gegenbeispiele liefern. In dieser Arbeit soll nun ein Werkzeug implementiert werden, das diese Gegenbeispiele rückübersetzt und dann durch Testen des Quellprogramms überprüft, ob die gelieferten Beispiele echte Gegenbeispiele sind, sodass die Programmiererin damit dann die zu beweisenden Programmeigenschaften verfeinern oder ändern kann.
Beinhaltet z.B.:
Eignung: Bachelor- oder Masterarbeit (je nach Umfang)
Von: Michael
Das bisherige Web-Framework Spicey basiert auf der Idee, automatisch aus einem Entity-Relationship-Modell eine Web-Anwendung zu generieren, mit dem man alle Entitäten und Relationen manipulieren kann. Mit diesem Web-Framework wurden verschiedene Web-Anwendungen erzeugt, wie z.B. die Moduldatenbank. Durch das neue Haskell-artige Typkonzept von Curry mit Typklassen kann der generierte Code vereinfacht und besser strukturiert werden. Dies soll in dieser Masterarbeit konzipiert und realisiert werden.
Beinhaltet:
Eignung: Masterarbeit
Von: Michael
Beinhaltet:
Eignung: Masterarbeit
Von: Michael
Beinhaltet:
Eignung: Bachelorarbeit
Von: Sandra
Das KiCS2 [1] kompiliert nach Haskell und erzeugt daher aus der FlatCurry-Darstellung Haskell-Code und übersetzt diesen erzeugten Code anschließend mit dem GHC [2]. Der GHC kann wiederum viele Optimierungen vornehmen. Aufgrund des Nichtdeterminismus der in Curry Bestandteil der Sprache ist, werden Curry-Datentypen und -Funktionen nicht 1-zu-1 in entsprechende Haskell-Konstrukte ersetzt. In dieser Arbeit soll evaluiert werden, welche Art von Curry-Programmen vom GHC optimiert werden können bzw. ob der generierte Code so "unnatürlich" ist, dass keine Optimierung zum Tragen kommt.
Beinhaltet:
Eignung: Bachelorarbeit (bei tatsächlicher "Lösung" des evaluierten Problems auch als Masterarbeit)
Von: Michael
Idee: Entwicklung und Implementierung von semantik-erhaltenden Optimierungen für FlatCurry als Bibliothek und/oder Binärprogramm
Beinhaltet:
Eignung: Masterarbeit
von: Sandra
Curr(y)gle ist eine Suchmaschine für Curry-Bibliotheken und deren Definitionen nach dem Vorbild von Hoogle [4], eine Suchmaschine aus der Haskell-Community.
Beinhaltet:
Eignung: Bachelorarbeit
[1] https://hackage.haskell.org/package/hoogle
[2] http://www.purescript.org
[3] http://elm-lang.org
[4] https://www.haskell.org/hoogle/
von: Michael
Beinhaltet:
Eignung: Masterarbeit
[1] http://doi.acm.org/10.1145/2505879.2505881
von: Michael
Beinhaltet:
Eignung: Bachelorarbeit (oder mit weiteren Themen evtl. Masterarbeit)
[1] http://www.purescript.org/
von: Michael
Beinhaltet:
Eignung: Masterarbeit
[1] http://www-ps.informatik.uni-kiel.de/currywiki/tools/oracle_debugger
von: Michael
Beinhaltet:
Eignung: Masterarbeit
von: Michael
Beinhaltet:
Eignung: Masterarbeit
[1] https://www.informatik.uni-kiel.de/~mh/lehre/abschlussarbeiten/msc/hueser.pdf
von: Michael
Beinhaltet:
Eignung: Masterarbeit
[1] http://www.informatik.uni-kiel.de/~mh/lehre/abschlussarbeiten/msc/holst.pdf
von: Michael
Beinhaltet:
Eignung: Bachelorarbeit
[1] http://www.informatik.uni-kiel.de/~mh/lehre/abschlussarbeiten/bsc/Sikorra.pdf
von: Michael
Beinhaltet:
Eignung: Bachelorarbeit (oder mit Erweiterungen auch Masterarbeit)
[1] http://www2.tcs.ifi.lmu.de/~abel/foetus.pdf
[1] http://www.cs.mcgill.ca/~dthibo1/papers/termination.pdf
von: Michael
Beinhaltet:
Eignung: Bachelorarbeit/Masterarbeit
Abschlussarbeiten mit anderen Kooperationspartnern sind (auch auf eigene Initiative) möglich. Hierzu sollte man Michael Hanus kontaktieren.