Theorie-Kolloquium
- Oberseminar, Prof. Dr. Kreitz, Dr. rer. nat. Richter, Di. 14:00-16:00, 3.04.2.01
In unserem Kolloquium diskutieren wir aktuelle Forschungsprojekte und -ergebnisse unserer Arbeitsgruppe und für unsere Arbeit relevante Ergebnisse aus den Bereichen Formale Methoden in der Programmierung sowie automatisches und taktikbasiertes Theorembeweisen.
09.07.: Lieven Leue: Security by Obscurity
am Beispiel der meistgenutzten Smartcard
Der Grundsatz "Sicherheit durch Unklarheit" widerspricht dem bereits 1883 formulierten Kerckhoffs'schen Prinzip, trotzdem wird er auch heute immer noch häufig verwendet. Warum dieser Ansatz nicht immer gut ist und welche Folgen er haben kann, soll anhand einer Smartcard erläutert werden.
02.07.: Tina Beigel: Formalisierung digitaler Spuren in der Forensik
Nach einer kurzen Einführung in die forensische Wissenschaft im Allgemeinen und die digitale Forensik im Besonderen möchte ich in meinem Vortrag ein formales System zur theoretischen Untermauerung der Computerforensik vorstellen. Ich stütze mich dabei auf die Dissertation von Andreas Dewald mit dem Titel "Formalisierung digitaler Spuren und ihre Einbettung in die Forensische Informatik".
25.06.: Edwin Brady (University of St. Andrews): Dependently typed functional programming with Idris
Idris is a general purpose pure functional programming language with dependent types. Its syntax is influenced by Haskell and its features include full dependent types and records, type classes, tactic based theorem proving, totality checking and an optimising compiler with a foreign function interface. One of the goals of the Idris project is to bring type-based program verification techniques to functional programmers while still supporting efficient systems programming via an optimising compiler and interaction with external libraries.
In this talk I will introduce dependently typed programming using Idris, and demonstrate its features using several examples including an interpreter for the simply typed lambda calculus, and a verified binary adder.
11.06: Mario Frank: Strukturelle und linguistische Selektion in großen Formelmengen
14.5. und 21.5: Sebastian Böhne:
Akzeptierbarkeit und ihre Relevanz für meine Arbeit
Hier die Folien des ersten Vortrags vom 14.5.
Und hier die Folien des zweiten Vortrags vom 21.5.
23.4., 30.4., 7.5.: Nuria Brede, Tim + Eva Richter:
zu Ralf Hinze: Generic Programming with adjunctions
In einer auf 3 Sitzungen geplanten Miniserie wollen wir uns mit dem Paper von Hinze beschäftigen. Hier der Abstract:
"Adjunctions are among the most important constructions in mathematics. These lecture notes show they are also highly relevant to datatype-generic programming. First, every fundamental datatype - sums, products, function types, recursive types - arises out of an adjunction. The defining properties of an adjunction give rise to well-known laws of the algebra of programming. Second, adjunctions are instrumental in unifying and generalising recursion schemes. We discuss a multitude of basic adjunctions and show that they are directly relevant to programming and to reasoning about programs."
In der ersten Sitzung geben wir, nach einer Presentation der grundlegenden Konzepte Kategorie, Funktor, natürliche Transformation im sog. "calculational style", die Definition, wichtige Eigenschaften und einige Beispiele von Adjunktionen.
