Hi *, am Mittwoch, 5. November 2014 treffen wir uns um 19.00 in India King für unser Hackathon. Bringt eure Laptops! Themen: - Agda: wir schreiben ein einfaches Hello World oder - Buch: Homotopy Type Theory (HoTT) -- BERICHT -- 26. Oktober 2014 - wir haben uns Categories for the working mathematician von Saunders Mac Lane angeschaut. - Das buch kann hier gefunden werden: www.maths.ed.ac.uk/~aar/papers/maclanecat.pdf die Datei kann man aber nicht durchsuchen weil es nur scans sind - dieses Buch ist eine grundlegende Arbeit in Kategorientheorie - das Text selbst ist sehr eigenständig; die Übungen machen aber annahmen über sehr viel Wissen in abstrakte Algebra - wir haben uns auch Category Theory von Steve Awodey angeschaut - das buch ist viel langsamer als Mac Lane. Man kommt nur nach mehreren Kapiteln zu interessanten Sachen - die Übungen basieren nur auf Wissen aus den Buch - das Buch ist einigermaßen kürzer als Mac Lane - wir haben uns auch Homotopy Type Theory (HoTT) angeschaut. Es kann hier gefunden werden: http://homotopytypetheory.org/book/ - thematisch ist das Buch zu den früheren beiden einigermaßen unterschiedlich: hier geht es um Logik und Typsysteme die von grund auf aufgebaut werden. Einige begriffe von Kategorientheorie werden eingeführt. - wobei Kategorientheorie das aller neuste vor 40 Jahren gewesen ist, ist HoTT zur Zeit so zu sagen der Stand der Technik - HoTT ist in sich komplett geschlossen. Es braucht nur sehr einfaches Basiswissen aus Grundlagen der Mathematik - Die Übungen basieren nur auf den Text und scheinen machbar zu sein - Einige der späteren Übungen sind aber offene Forschungsprobleme - Das buch ist so lange wie Mac Lane und Awodey zusammen - Es wird von einer großen Gruppe von Experten geschrieben, unter anderem Martin-Löf, Awodey, Aczel. Es wird ständig aktiv erweitert. - Für HoTT kann man in Internet Code für Coq und Agda finden - Es gibt auch aktive online Communities für HoTT - wir werden in der Zukunft wahrscheinlich viel über HoTT und theorem prover sprechen -- ANFAHRT -- Wir treffen uns in India King, Landsbergerstr. 491. Webseite: http://www.indiaking.de Karte: https://goo.gl/maps/5g9m6 Anfahrtmöglichkeiten: - S-Bahn nach Pasing nehmen (alle außer S1, S2 und S7) und dann Tram 19 nach Offenbachstraße (2 Haltestellen) - Tram 19 von Hauptbahnhof richtung Pasing nehmen bis Offenbachstraße - Bus 130 oder 131 zum Knie nehmen und dort in die Tram 19 nach Pasing umsteigen, bis Offenbachstraße - Bus 160 oder 162 nach Offenbachstraße India King befindet sich genau gegenüber der Tramhaltestelle. Twitter: https://twitter.com/Haskell_hackers Web: http://haskell-hackathon.no-ip.org English: http://haskell-hackathon.no-ip.org/index_en.html