Prof. Dr. Nadine Dittert, Forschungssgruppe Informatik und ihre Didaktik, Institut für Informatik, Universität Koblenz:
TBA
Dr. Christoph Lenzen, Forschungsgruppe Algorithmische Grundlagen und Kryptographie, CISPA Helmholtz-Zentrum für Informationssicherheit, Saarbrücken:
Sich einigen ist bereits schwer genug, wenn alle an einem Strang ziehen! Doch was passiert, wenn einzelne Parteien dies verhindern wollen, ohne Rücksicht auf Verluste? Dieser Workshop gewährt einen Einblick in verteilte algorithmische Ansätze, diesem Problem zu begegnen. Dies hat Alltagsrelevanz in technischen Bereichen - zum Beispiel der elektronischen Steuerung von Autos und Flugzeugen - aber auch demokratischen Systemen.
Dr. Anna-Lena Lorenz, Open Research Knowledge Graph, TIB Leibniz-Informationszentrum Technik & Naturwissenschaften, Hannover:
TBA
Prof. Dr. Annette Bieniusa, Lehrstuhl Software Technology: Programming Distributed Systems, Fachbereich Informatik, Rheinland-Pfälzische Technische Universität Kaiserslautern-Landau, Kaiserslautern:
TBA
Prof. Dr. Sebastian Hack, Compiler Design Lab, Saarland Informatics Campus, Universität des Saarlandes, Saarbrücken:
Beweisassistenten sind Programme, mit denen man mathematische Beweise führen und verifizieren kann. Der Beweisassistent stellt sicher, dass der geführte Beweis tatsächlich die zu zeigende Aussage beweist. Beweisassistenten spielen eine immer größere Rolle in der Verifikation von Software- und Hardwaresystemen und leisten damit einen wichtigen Beitrag zur Zuverlässigkeit von modernen Computersystemen. Aber auch in der Mathematik werden zunehmend wichtige Beweise mit Beweisassistenten verifiziert.
Modernen Beweisassistenten liegt der sogenannte Curry-Howard Isomorphismus zu Grunde, eine Isomorphie zwischen höherstufiger Logik und Programmiersprachen. Somit gibt es eine interessante Analogie zwischen dem Beweisen von mathematischen Aussagen und dem Programmieren.
In diesem Workshop möchte eine kleine Einführung in die dem zugrunde liegenden Konzepte und eine praktische Einführung in den populären Beweisassistenten Coq geben.
Wenn Sie möchten, bringen Sie gerne ihr Notebook mit. Wir werden gemeinsam durch kleinere Coq Beweise gehen. Dazu muss man nichts installieren, alles läuft im Browser.