Prof. Dr. Nadine Dittert, Forschungssgruppe Informatik und ihre Didaktik, Institut für Informatik, Universität Koblenz:
Making lässt Schüler:innen zu Erfinder:innen innen werden, lässt sie die digitale Welt mitgestalten und ermöglicht ihnen, diese durch aktives Handeln zu verstehen. Während oft ein ästhetisch ansprechendes Produkt entsteht, ist es vor allem der Prozess dorthin, der für das Lernen relevant ist. Making für den schulischen Kontext ist bisher eher durch einen klar definierten Prozess zu einem gezielten Produkt gekennzeichnet. Dies macht die Aktivität organisatorisch wie inhaltlich planbar und gibt Sicherheit. Maker-Bildung beschreibt darüber hinaus auch einen offenen Prozess, in dem Lernwege und Ergebnisse nicht vordefiniert sind und in dem Fehler, Um- und Weiterdenken erlaubt und erwünscht sind.
Im Vortrag betrachten wir Making aus der Informatikperspektive heraus und möchten anhand konkreter Beispiele Herausforderungen und Chancen herausstellen, die die Kombination mit sich bringt.
Dr. Christoph Lenzen, Forschungsgruppe Algorithmische Grundlagen und Kryptographie, CISPA Helmholtz-Zentrum für Informationssicherheit, St. Ingbert:
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:
Die Wissenschaft steht vor einer Herausforderung: Aufgrund der stetig wachsenden Flut an Veröffentlichungen fällt es vielen Forschenden schwer, einen Überblick über relevante Beiträge zu ihrem Gebiet zu behalten. Hier schafft der ORKG Abhilfe.
Mit einer Kombination aus großen Sprachmodellen und Wissensgraphen bietet der ORKG Forschenden maschinelle Unterstützung auf der Suche nach Informationen. Das neue Tool ORKG Ask setzt dabei auf KI und extrahiert Wissen aus Publikationen. Dank einer übersichtlichen Ausgabe ist es nicht nur Forschenden selbst, sondern auch der interessierten Öffentlichkeit so möglich, ihre Fragen an die Wissenschaft zu stellen. Der Wissensgraph ORKG geht noch einen Schritt weiter und stellt relevante Beiträge direkt in einem maschinenlesbaren Format dar. Gemeinsam schaffen KI und Wissensgraphen so die Grundlage für einen modernen wissenschaftlichen Austausch.
Prof. Dr. Annette Bieniusa, Lehrstuhl Software Technology: Programming Distributed Systems, Fachbereich Informatik, Rheinland-Pfälzische Technische Universität Kaiserslautern-Landau, Kaiserslautern:
Apps speichern unsere Daten oft in der Cloud auf weltweit verteilten Servern. Dies verringert die Wahrscheinlichkeit von Datenverlust und ermöglicht es uns Dokumente, Fotos, Spielzustände etc. mit anderen zu teilen. Es erlaubt aber auch, detaillierte Informationen über Nutzer zu sammeln und deren Verhalten zu analysieren. Wenn es Probleme bei der Netzwerkverbindung gibt, können wir solche Apps nicht nutzen. Und wenn der Anbieter die Anwendung nicht mehr bereitstellt, sind die Nutzerdaten (meist) einfach weg.
Local-first Software durchbricht die Abhängigkeit von der Cloud. Techniken wie konflikt-freie replizierte Datentypen (CRDTs) ermöglichen dabei auch ohne zentralen Server die Kollaboration von Nutzern an gemeinsamen Dokumenten. In diesem Vortrag betrachten wir die alten und neuen Ideen hinter dem aktuellen Trend in der Software-Entwicklung.
Wir stellen dazu auch Demos zur Verfügung, mit denen Sie im Browser experimentieren können.
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.