Links und Funktionen
Sprachumschaltung

Navigationspfad
Sie sind hier: Startseite / Lehre / WS 2018/19 / Oberseminar / Andreas Abel: Beweis-relevante Prädikate und Evidenz-verwaltende Programmierung


Inhaltsbereich

Andreas Abel: Beweis-relevante Prädikate und Evidenz-verwaltende Programmierung

Oberseminarvortrag von Andreas Abel über Beweis-relevante Prädikate und Evidenz-verwaltende Programmierung
Wann 14:15 16:00 11.01.2019
von bis
Wo Raum L109, Oettingenstr. 67
Termin übernehmen vCal
iCal

Es spricht Andreas Abel über:
Beweis-relevante Prädikate und Evidenz-verwaltende Programmierung

Abstract:
Wir betrachten einige Beispiele für Prädikate und Relationen, deren
Herleitungen (Beweis) interessante Informationen enthalten.  Z.B. ist
der Beweis der Mitgliedschaft eines Elementes in einer Liste ein
Zeiger auf dessen Position;  der Beweis der Mitgliedschaft eines
Wortes in einer formalen Sprache ist ein Parse-Baum.

Wir stellen uns weiterhin die Frage, wie wir Programme und Datentypen
strukturieren können, so dass Evidenz für berechnete Eigenschaften
für künfigte Berechnungen verfügbar bleibt.  Z.B. wissen wir nach
erfolgreicher Typprüfung eines Ausdrucks, dass der Ausdruck
wohlgetypt ist, d.h. bestimmte Formen nicht annehmen kann.  Diese
Information kann spätere Berechnungsschritte erleichtern, z.B. die
Auswertung des Ausdrucks.  Das Behalten und Verwalten berechneter
Evidenz nennen wir "Evidenz-verwaltende Programmierung".

Falls Zeit ist, werde ich eine grössere Fallstudie vorstellen: die
Implementierung eines Fragmentes der Sprache C.

Artikelaktionen


Funktionsleiste