BEGIN:VCALENDAR
VERSION:2.0
PRODID:ILLC Website
X-WR-TIMEZONE:Europe/Amsterdam
BEGIN:VTIMEZONE
TZID:Europe/Amsterdam
X-LIC-LOCATION:Europe/Amsterdam
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:19700329T020000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:19701025T030000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
UID:/NewsandEvents/Archives/2025/newsitem/15927/11
 -December-2025-Introduction-to-Type-Theory-by-Thor
 sten-Altenkirch-University-of-Nottingham-
DTSTAMP:20251201T152819
SUMMARY:Introduction to Type Theory by Thorsten Al
 tenkirch (University of Nottingham)
DTSTART;VALUE=DATE:20251211
DTEND;VALUE=DATE:20251211
LOCATION:Alsterterrasse 1, 20354 Hamburg [D]
DESCRIPTION:In this course we will use the Agda sy
 stem to explore the central concepts of Type Theor
 y. Topics include dependent types, dependent funct
 ions, propositions-as-types, and formal reasoning 
 within type theory. If time permits, we will also 
 discuss recent developments such as Homotopy Type 
 Theory and its implementation in Cubical Agda. Thi
 s is an introductory lecture - no previous knowled
 ge of Type Theory is required.  Registrations are 
 accepted on a rolling basis, spots are limited.
X-ALT-DESC;FMTTYPE=text/html:\n  <p>In this course
  we will use the Agda system to explore the centra
 l concepts of Type Theory. Topics include dependen
 t types, dependent functions, propositions-as-type
 s, and formal reasoning within type theory. If tim
 e permits, we will also discuss recent development
 s such as Homotopy Type Theory and its implementat
 ion in Cubical Agda. This is an introductory lectu
 re - no previous knowledge of Type Theory is requi
 red.</p>\n  <p>Registrations are accepted on a rol
 ling basis, spots are limited.</p>\n
URL:https://sites.google.com/view/mc-intro-tt-by-t
 a/
CONTACT:Deniz Sarikaya at d.sarikaya at uni-luebec
 k.de
END:VEVENT
END:VCALENDAR