[Munich-lisp] Haskell Hackathon Mittwoch, 5.11.2014 - Agda, HoTT

[Haskell Hackathon]

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