BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//pretalx//cfp.gulas.ch//WWMGVN
BEGIN:VTIMEZONE
TZID:CET
BEGIN:STANDARD
DTSTART:20001029T040000
RRULE:FREQ=YEARLY;BYDAY=-1SU;BYMONTH=10
TZNAME:CET
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
DTSTART:20000326T030000
RRULE:FREQ=YEARLY;BYDAY=-1SU;BYMONTH=3
TZNAME:CEST
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
END:VTIMEZONE
BEGIN:VEVENT
UID:pretalx-gpn22-WWMGVN@cfp.gulas.ch
DTSTART;TZID=CET:20240531T143000
DTEND;TZID=CET:20240531T153000
DESCRIPTION:Type theory is the secret sauce that makes a programming langua
 ge awesome. The more knowledge we can make the compiler aware of\, the mor
 e we can rely on the compiler.\n\nBut what is the limit? What if we could 
 take _make bad state unrepresentable_ to the mathematical extreme? What is
  a proof anyway\, can you eat it? Come on a wonderful journey into the lan
 d of dependent types\, where we try building type-safe SQL queries\, and s
 weeten the deal with our own syntactic sugar.
DTSTAMP:20240520T164255Z
LOCATION:ZKM Vortragsraum
SUMMARY:Intro to Lean 4: A language at the intersection of programming and 
 mathematics - Kiiya
URL:https://cfp.gulas.ch/gpn22/talk/WWMGVN/
END:VEVENT
END:VCALENDAR