Informatik-Kolloquium

Vortrag im Rahmen des Informatik-Kolloquiums

Lazy Evaluation in der computergestützten Komposition

Vortragender: Diplom Komponist Kilian Sprotte

am Mittwoch, 10.03.2010, 13:30 Uhr, Hauptgebäude, Raum 2.44

Zusammenfassung:

Grafische Programmiersprachen, die in der Form von Blockdiagrammen die Modellierung musikalischer Prozesse erlauben, finden bereits häufig Verwendung. Sie lassen sich grob in zwei Gruppen einteilen. Auf der einen Seite ist ein System wie "Pure Data" überwiegend zur Klangsynthese geeignet, während auf der anderen Seite eine Kompositionsumgebung wie "OpenMusic" oder "PWGL" die Arbeit an übergeordneten Strukturen, angefangen bei Notenereignissen bis zur globalen Form erlaubt.
Es wird ein Prototyp einer solchen grafischen Programmiersprache vorgestellt, die in Lisp eingebettet ist, aber auf einem Lazy Dialekt aufsetzt und prinzipiell beide Anwendungsgebiete vereint. Dazu werden Beispiele gezeigt und auch verschiedene Datenstrukturen zur Musikrepräsentation vorgestellt.

Short Bio:

Kilian Sprotte studierte Komposition bei Prof. Younghi Pagh-Paan und Elektronische Musik bei Günter Steinke an der HfK Bremen. Zu seinen Werken gehören überwiegend instrumentale Kompositionen, aber auch Klanginstallationen und Arbeiten mit Video.
Er interessierte sich zunehmend für die computergestützte Komposition, wurde am IRCAM, Paris für ein Jahr in die Music Representation Group als Gastforscher eingeladen und hat seitdem in verschiedenen - überwiegend lisp-basierten - Softwareprojekten mitgewirkt, so auch seit 2007 an der Kompositions-umgebung PWGL.

Vortrag im Rahmen des Informatik-Kolloquiums

Model Checking als Ansatz zur Verifikation digitaler und eingebetteter Systeme

Vortragender: Dipl.-Ing. Thilo Vörtler

am Donnerstag, 04.03.2010, 11:00 Uhr, Hauptgebäude, Raum 2.13

Zusammenfassung:

Eingebettete Systeme bestehen meist aus einer Kombination von  Hardware,
Software und Sensoren. Sie werden in einer Vielzahl von Anwendungsbereichen und Geräten verwendet, z.B. in der Automobilbranche oder der Medizintechnik.
Model Checking ist eine Verifikationstechnik die es erlaubt, die funktionale Korrektheit nicht nur durch Simulation zu überprüfen, sondern die Korrektheit von Systemeigenschaften zu beweisen. Beim Entwurf digitaler Schaltungen wird Model Checking, ergänzend zur Simulation, als Methode zur Überprüfung von kritischen Eigenschaften bereits verwendet. Auch für die Verifikation von Software eines eingebetteten Systems lässt sich Model Checking verwenden, wobei insbesondere die Verifikation im Zusammenspiel mit Hardware eine Herausforderung darstellt.

Im Vortrag wird Model Checking als Methode zur Verifikation von digitalen Systemen vorgestellt. Es werden praktische Probleme erläutert, welche bei der Verifikation von Digitalentwürfen auftreten. Außerdem wird Software Model Checking vorgestellt, welche es ermöglicht Software für eingebettete Systeme zu überprüfen.

Vortrag im Rahmen des Informatik-Kolloquiums

Beispielgetriebene Schemainduktion beim induktiven Programmieren

Vortragender: Dipl.-Wirtsch.Inf. (E.M.B.Sc.) Martin Hofmann
Otto-Friedrich-Universität Bamberg

am Mittwoch, 27.1.2010, 14:00 Uhr, Hauptgebäude, Raum 2.13

Zusammenfassung

Induktives Programmieren (IP) beschäftigt sich mit dem Erzeugen (rekursiver) Programme aus unvollständigen Spezifikationen, in der Regel Eingabe- / Ausgabebeispielen. Alle bekannten IP Algorithmen können als Suche im Raum aller Kandidatenprogramme aufgefasst werden, mit folglich exponentiellem Aufwand.

Um den Suchaufwand zu beschränken und den Suchraum zu reduzieren, können Programmschemata verwendet werden. Allerdings muss entweder ein (oft sehr gut) informierter Benutzer ein Schema a priori vorgeben, oder verschiedene Schemata werden einfach wahllos ausprobiert. In der anschließenden Synthese werden nun alle Daten in Hinblick auf dieses eine gegebene Schema interpretiert welches folglich nun gewissermaßen ausschließlich über Erfolg oder Misserfolg entscheidet.

Anstelle nun die gegebenen Daten „in ein Schema zu pressen“, stellen wir einen Ansatz vor, der es erlaubt anhand der Daten ein Schema zu induzieren. Wir nutzen dazu universelle Eigenschaften von Funktionen höherer Ordnung, die sich in den Eingabe- /Ausgabedaten finden lassen. Diese Technik erlaubt es uns, Catamorphismen auf allgemeinen algebraischen Datenstrukturen in unserem IP System Igor2 einzuführen.

Vortrag im Rahmen des Lehrstuhl-Kolloquiums

Generische Record-Kombinatoren mit statischer Typprüfung

Vortragender: Dipl.-Inf. Wolfgang Jeltsch

am 13.01.2010, 13:45 Uhr, Hauptgebäude, Raum 2.13

Zusammenfassung

Records, d.h. Kollektionen von benannten Feldern, sind ein wesentlicher Bestandteil vieler Programmiersprachen. Neben dem Zugriff auf einzelne Felder spielen dabei Operationen auf gesamten Records, sogenannte Kombinatoren, eine wichtige Rolle. Record-Kombinatoren müssen oftmals generisch sein, also mit Records verschiedener Struktur arbeiten. Generische Record-Kombinatoren können im Allgemeinen nur in dynamisch typisierten Sprachen definiert werden.

In dem Vortrag wird ein Record-System für die Programmiersprache Haskell vorgestellt, welches die Definition statisch typisierter generischer Record-Kombinatoren ermöglicht. Dieses System ist als Bibliothek implementiert, kommt also ohne Änderungen an der Programmiersprache aus. Ermöglicht wird das vor allem durch die Nutzung fortgeschrittener Typsystemkonzepte.

Vortrag im Rahmen des Informatik-Kolloquiums

Programmierung und Verifikation reaktiver Systeme mittels funktionaler Programmierung

Vortragender: Dipl.-Inf. Wolfgang Jeltsch

am 18.11.2009, 13:45 Uhr, Hauptgebäude, Raum 2.13

Zusammenfassung

Funktionale Reaktive Programmierung (FRP) ist ein Paradigma, mit dessen Hilfe reaktive und interaktive Systeme deklarativ programmiert werden können. Der Programmierer beschreibt zeitliches Verhalten von Systemkomponenten mittels kontinuierlicher und diskreter Signale, welche zeitveränderliche Werte bzw. Ereignisfolgen darstellen. Dabei können durch Signal-Operatoren aus einfachen Signalen komplexe Signale aufgebaut werden.

Der Vortrag gibt zunächst eine Einführung in die Grundkonzepte von FRP. Anschließend behandelt er typische Probleme der Implementierung von FRP-Bibliotheken und zeigt Lösungen auf. Schließlich geht er auf die enge Beziehung zwischen FRP und temporaler Logik ein und deutet an, wie diese für die Verifikation reaktiver Systeme nutzbar gemacht werden kann.