November 2014 - munich-lisp - mailman3.common-lisp.net

[Munich-lisp] Haskell Hackathon 30.11.2014 12:00 - Agda, HoTT, Android
by Haskell Hackathon 29 Nov '14

29 Nov '14

Hi *, am Sonntag, 30. November 2014 treffen wir uns um 12:00 in India King für unser Hackathon. Bringt eure Laptops! Themen: - Agda: wir machen weiter mit den Agda-Tutorial: http://oxij.org/note/BrutalDepTypes/ oder - Buch: Homotopy Type Theory (HoTT) oder - wir hacken ein bisschen an Android rum, um später ein Haskell DSL zu schreiben welches auf Android Apps runterkompiliert -- BERICHT -- 16. November 2014 - über Agda gesprochen und darüber, was Theorem Prover sind - wofür die gut sind - Haskell installiert - Agda installiert - Emacs installiert und für Agda konfiguriert -- 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

1 0

[Munich-lisp] Munich Haskell Meeting, 2014-11-26 @ 19:30
by Christian Neukirchen 23 Nov '14

23 Nov '14

Dear all, next week, on Wednesday, 26th of November, our monthly Munich Haskell Meeting will take place again at Cafe Puck at 19:30 CET. For details see here: http://www.haskell-munich.de/dates Since Heinrich is not around much in Munich anymore, I have taken over organizing our Haskell meeting. The website will be updated soon. For the meantime, if you plan to join, please add yourself to this dudle so we can reserve enough seats: https://dudle.inf.tu-dresden.de/haskell-munich-nov-2014/ Everybody is welcome! Looking forward to see you, -- Christian Neukirchen <chneukirchen(a)gmail.com> http://chneukirchen.org

1 0

[Munich-lisp] Haskell Hackathon 23.11.2014 - Agda, HoTT, Android
by Haskell Hackathon 22 Nov '14

22 Nov '14

Hi *, am Sonntag, 23. November 2014 treffen wir uns um 16:00 in India King für unser Hackathon. Bringt eure Laptops! Themen: - Agda: wir versuchen ein einfaches Programm zu schreiben oder - Buch: Homotopy Type Theory (HoTT) oder - wir hacken ein bisschen an Android rum, um später ein Haskell DSL zu schreiben welches auf Android Apps runterkompiliert -- BERICHT -- 5. November 2014 - wir haben Agda 2.4.2 installiert. Es hat ein paar Probleme auf Grund von cabal gegeben, die konnte man aber lösen indem man --constraint benutzt hat. - man kann Agda übrigens auch im sandbox installieren - einer von uns hat zuvor Agda 2.3.2 aus einen .deb installiert. Das hat auch einige haskell-libraries zurückgelassen; nach deren entfernung waren die noch im ghc index vorhanden, aber kaputt (.so Dateien nicht vorhanden). Das haben wir mit cabal install --reinstall gelöst. - man muss zuerst das agda-mode Plugin für Emacs installieren: agda-mode setup - danach muss man die stlib runterladen: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary - und das src von stdlib Unterverzeichnis in Emacs als include-path für agda2-mode hinterlegen: in Emacs über M-x customize-group RET agda2 RET - wir haben ein einfaches Tutorial angefangen: http://www.stephendiehl.com/posts/agda.html - es gibt auch "agda summer school": https://github.com/UlfNorell/agda-summer-school/ -- die benutzte library ("agda prelude") ist aber mit der stdlib von Agda inkompatibel - wir haben über online-foren für HoTT gesprochen: "hott amateurs": https://groups.google.com/forum/#!forum/hott-amateurs das offizielle Forum für HoTT: https://groups.google.com/forum/#!forum/homotopytypetheory IRC: ##hott auf Freenode -- 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

1 0

[Munich-lisp] Haskell Hackathon 16.11.2014 - theorem provers, HoTT, Android
by Haskell Hackathon 15 Nov '14

15 Nov '14

Hi *, am Sonntag, 16. November 2014 treffen wir uns um 16:00 in India King für unser Hackathon. Bringt eure Laptops! Themen: - Agda: wir versuchen ein einfaches Programm zu schreiben oder - Buch: Homotopy Type Theory (HoTT) oder - wir hacken ein bisschen an Android rum, um später ein Haskell DSL zu schreiben welches auf Android Apps runterkompiliert -- BERICHT -- 2. November 2014 - wir haben HoTT gelesen - wir haben uns theorem prover angeschaut und vergliechen: Agda, Coq, Isabelle/HOL, Idris. - Nur Agda und Coq sind für HoTT nutzbar - Idris und Isabelle/HOL sind aber für viele Sachen viel mehr praktisch -- 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

1 0

[Munich-lisp] Haskell Hackathon Mittwoch, 5.11.2014 - Agda, HoTT
by Haskell Hackathon 04 Nov '14

04 Nov '14

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

1 0

[Munich-lisp] Haskell Hackathon 2.11.2014 - theorem provers, HoTT
by Haskell Hackathon 01 Nov '14

01 Nov '14

Hi *, am Sonntag, 2. November 2014 treffen wir uns um 18.00 in India King für unser Hackathon. Bringt eure Laptops! Die Hackathon-webseite ist jetzt auch auf Englisch! Das waren rund 100k text zu übersetzen... Viel spaß beim lesen! http://haskell-hackathon.no-ip.org/index_en.html Themen: - proof systems: Isabelle/HOL, Agda, Coq oder - Buch: Homotopy Type Theory (HoTT) -- BERICHT -- 16. Oktober 2014 - ein Paar der Klasseninstanzen angeschaut: identitätsmonade, funktoren und monoid für funktionen, ... - mit Christine darüber gesprochen, wie man ein beginner-kurs für Haskell betreiben könnte. Eine Idee war es, ein Buch in einer Gruppe durchzulesen. Eine weitere Idee war es, Tutorials eins nach dem anderen durchzugehen. Man könnte auch Übungen machen. - darüber gesprochen, wie man eine Community betreiben soll; wie sie sich entwickelt und wie man es schafft den zutritt neuer Teilnehmer nicht zu verhindern. - das Buch "Haskell-Intensivkurs" durchgeschaut: http://www.amazon.de/Haskell-Intensivkurs-Kompakter-Funktionale-Programmier… -- 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

1 0