Das wird heiß

Makarius

Das Treffen für Haskellistas, Scalafisten, Lambdroiden und andere funktionale, kohlenstoffbasierte Lebensformen in Augsburg!

Der Curry Club soll Treffpunkt sein, um Konzepte und Ansätze, Praktisches und Abstraktes, Purität und Effekte, Faulheit und Striktheit, Monaden und Monoide und sonst auch wirklich alles passende zu diskutieren.

Die Idee, einen funktionalen Stammtisch zu gründen, kam auf der ersten Augsburger Nerdnacht auf.

Wir treffen uns im vierwöchigen Turnus, das nächste Mal am

Donnerstag, den 14.07.2016, 19:00 Uhr MESZ.

In einem Wiki sammeln wir Themenvorschläge.

Programm für das sechzehnte Treffen am 14. Juli 2016

Makarius stellt Cobra vor, ein modernes Framework, um Code und Beweise zu präsentieren. Cobra unterstützt Isabelle-Beweise sowie Scala- und Haskell-Code.

Profpatsch teilt seine Beobachtung, dass Zipper zu den coolsten Datenstrukturen gehören, und wird damit die Reihe über funktionale Datenstrukturen fortsetzen.

Bei diesem oder dem nächsten Treffen wird Tim einen Vortrag zu Versionskontrollsystemen und Patch-Theorie halten. Er wird darin die unterschiedlichen Modelle von git, darcs und insbesondere dem neuen Versionskontrollsystem Pijul vorstellen. Letzteres VCS basiert auf (oder ist laut Webseite “inspiriert von”) einer kategorientheoretischen Theorie von Patches von Samuel Mimram und Cinzia Di Giusto.

[Kurze Werbepause: Das Paper ist richtig cool! Die Autoren gehen von der Kategorie der “normalen”, linearen Dokumente aus und wollen dann “mergen” als Pushout modellieren. Damit Patches immer gemergt werden können, sollte die Kategorie endlich kovollständig sein, damit alle Pushouts existieren. Deshalb gehen die Autoren zur freien konservativen (schon existierende Kolimiten bleiben erhalten) Kovervollständigung der Kategorie der linearen Dokumente über. Diese Kovervollständigung man nach einem Folklore-Theorem explizit als volle Unterkategorie der Kategorie der Prägarben auf der Kategorie der linearen Dokumente beschreiben. Im Hauptteil des Papers leiten die Autoren eine viel konkretere, graphentheoretische Beschreibung dieser Kategorie her.]

Ingo beginnt unter dem Titel Was sind und was sollen die Typen? eine Einführung in Typtheorie unter besonderer Beachtung von Homotopietyptheorie. Die grundlegende Motivation aus der Informatik und der Programmierpraxis sind natürlich bekannt: Man möchte zur Compilezeit Informationen über das Programmverhalten gewinnen, um fehlerhafte Programme noch vor ihrer Ausführung erkennen und ablehnen zu können.

Aber es ist vielleicht weniger bekannt, wie Typtheorie entstanden ist (das war nämlich lange vor den Programmiersprachen), welches Problem sie ursprünglich lösen sollte (und auch tatsächlich löst), und wie ein Typsystem aufgebaut ist.

Ziel des ersten Teils wird auch sein, ein Grundverständnis im Lesen von Typsystemspezifikationen zu vermitteln. Wir werden extensionale und intensionale Martin-Löf-Typtheorie behandeln.

Homotopietyptheorie ist ein neuer Zweig der Mathematik, der Aspekte von verschiedenen anderen Teilgebieten der Mathematik auf verblüffende Art und Weise kombiniert. Es ist Teil von Voevoedskys Programm zu einer univalenten Grundlegung der Mathematik und basiert auf einer kürzlich entdeckten Verbindung zwischen Homotopietheorie aus der Mathematik und Typtheorie aus der Logik und theoretischen Informatik.

In gewöhnlichen Zugängen zu einer Grundlegung der Mathematik unterscheidet man zwischen Objekten (wie zum Beispiel natürlichen Zahlen und Mengen) und Aussagen über diese Objekte. In Homotopietyptheorie gibt es diese Unterscheidung nicht. Objekte und Aussagen über Objekte werden auf eine gemeinsame Stufe gestellt. Beweisen und Konstruieren werden miteinander identifiziert.

Der Vortrag setzt keine Vorkenntnisse aus Logik und Typtheorie und selbstverständlich auch keine aus Homotopietheorie voraus. Der Vortrag ist für Leute konzipiert, die sich für diese neue Bewegung in der Logik interessieren, aber nicht praktizierende Mathematikerinnen sind.

Er wird folgende Fragen klären: Was hat es mit Homotopietyptheorie auf sich? Wie werden in Homotopietyptheorie Objekte und Aussagen miteinander vereint, auf eine Stufe gestellt? Wozu ist Homotopietyptheorie gut? Wieso und für wen ist sie interessant?

Ein Teil der Antwort auf die letzte Frage lautet: Homotopietyptheorie ist für Leute interessant, die computergestützt Beweise führen möchten.

Programm für das siebzehnte Treffen am 11. August 2016

Programm für das achtzehnte Treffen am 8. September 2016

Marc wird voraussichtlich über Hygienische Makros: Praxis, Theorie und Implementierung am Beispiel von Scheme sprechen.

Du schreibst ein cooles Haskell-Projekt, hast eine tolle neue funktionale Programmiersprache entdeckt, oder verstehst endlich, wie SchachGo-AIs funktionieren? Dann halte einen Vortrag! Die Organisation geht über unsere Mailingliste.

Kurzvorträge (< 10 min) können auch unangekündigt gehalten werden, in Absprache mit der jeweiligen Organisatorin.

Treffen & Veranstaltungen