Praktikum Mathematische Logik (Bachelor-Modul P2A1, 9LP, 270h)

Topic: Natural Isabelle

Dozenten

Prof. Dr. Peter Koepke
Dr. Ioanna Dimitriou

Zeit und Ort

Wochentliches Treffen: jeden Donnerstag 16:00-18:00 im Seminarraum 0.003 (außer den 3.12., siehe Tutoriumsreihe unten).
Die Teilnehmer des Praktikums können im Praktikumszimmer N1.007 arbeiten, wo relevante Bücher, Artikel, und Frau Dimitrious Hilfe stehen.

Erstes & zweites Treffen:
Beim 1. bzw. 2. Treffen des Hauptseminars mathematische Logik, Dienstag den 27. Oktober bzw. 3. November, 14:00-16:00, im Zimmer N0.008.

Am 03. und 04. Dezember werden wir eine Tutoriumsreihe von Dr. Markus Makarius Wenzel veranstalten.

Alle Teilnehmer sollten diese Webseite beobachten:
http://sketis.net/2015/isabelle-tutorial-at-bonn
und die gesonderte Isabelle-Version installieren, die in diese Webseite steht.

Das Programm für diese Tage:

Donnerstag 03. Dezember 2015
Alle Tutorien werden im Besprechungsraum 2.025 (IAM) stattfinden.

12:30 -- 14:00: Tutorium
14:30 -- 16:00: Tutorium
16:30 -- 18:00: Tutorium

Freitag 04. Dezember 2015
Der Oberseminarvortrag und alle Tutorien werden im SR. 2.008 (MI) stattinden.

10:00 -- 11:30: Oberseminar Vortrag
11:30 -- 12:30: Mittagessen Mensa
12:30 -- 14:00: Tutorium
14:30 -- 16:00: Tutorium
16:30 -- 18:00: Tutorium

Inhalt

Wir werden uns mit dem Erstellen einer LaTeX-Oberfläche für den Beweis-Assistenten Isabelle/Isar beschäftigen. Da diese mittels der einfachen funktionalen Sprache OCaml erstellt werden soll, empfehlen wir den Praktikumsteilnehmern, sich bei folgenden Online-Kurs anzumelden:
MOOC « Introduction to functional programming in OCaml »
der zum Beginn des Semesters (19. Oktober 2015) anfängt.

Eine kurze Einleitung zur OCaml wird auch in den ersten zwei Terminen des Hauptseminars Mathematische Logik stattfinden.

Teilnehmer