Hi *,
am Sonntag, 28. Dezember 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)
-- BERICHT --
14. Dezember 2014
- über das "mutual" keyword in Agda gelernt
- die kommutativität einer eigenschaft in einem beweis benutzt
- induktive beweise benutzt
- über negative beweise gelernt
- über elimination gelernt
-- 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
Hi *,
am Sonntag, 21. Dezember 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 --
7. Dezember 2014
- Über holes in Agda gelernt
- agda-mode tastaturkommandos durchgeschaut
- Die automatisierte beweisfunktionen von Agda ausprobiert
- Auf mehrere Weisen ein induktives Beweis in Agda durchgeführt
-- 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
Hi *,
am Sonntag, 14. Dezember 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 --
30. November 2014
- Mit den Agda-Tutorial weitergemacht!
- ein Paar neue Kommandos in emacs gelernt
-- 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
Hi *,
am Sonntag, 6. Dezember 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 --
23. November 2014
- über Gödel's Reise nach USA gesprochen, und dass er in der U.S.
Verfassung Inkonsistenzen gefunden hat... Einstein und die anderen
mussten aufpassen, dass er das vorm Immigrationsdienstbeahmten nicht
erwähnt!
- über Gödel's Unvollständigkeitssatz, und den Zusammenhang mit
ZFC-mengenlehre, Typentheorie, HoTT gesprochen
- darüber gesprochen, was es für praktische Anwendungen für
Beweissysteme in der Industrie gibt
- ein gutes Tutorial für Agda gefunden: http://oxij.org/note/BrutalDepTypes/
- über Haskel Curry und die Curry-Howard Korrespondenz gesprochen
- wir sind im Tutorial bis zu implicit parameters und forall gekommen
- wir haben über den Klaus sein Job im Bank gesprochen und auf welche
Weisen man die Zusammenhänge zwischen Bankkonten abbilden könnte
- über Bigraphen gesprochen
-- 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