BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Drupal iCal API//EN
X-WR-CALNAME:Events items teaser
X-WR-TIMEZONE:America/Toronto
BEGIN:VTIMEZONE
TZID:America/Toronto
X-LIC-LOCATION:America/Toronto
BEGIN:DAYLIGHT
TZNAME:EDT
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
DTSTART:20250309T070000
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:EST
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
DTSTART:20241103T060000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
UID:69f57a7a72985
DTSTART;TZID=America/Toronto:20250919T143000
SEQUENCE:0
TRANSP:TRANSPARENT
DTEND;TZID=America/Toronto:20250919T153000
URL:https://uwaterloo.ca/pure-mathematics/events/logic-seminar-77
SUMMARY:Logic Seminar
CLASS:PUBLIC
DESCRIPTION:ELAN ROTH\, UNIVERSITY OF PENNSYLVANIA\n\n_Formalizing Turing R
 eductions in Lean_\n\nTuring Reducibility and Turing Degrees simply charac
 terize how\ndifficult problems in mathematics are. We will begin by review
 ing\nreductions and degrees\, situating the degree structure as a partial\
 norder with a central spine of relativized halting problems. Then\, we\nwi
 ll explore Lean as a functional programming language and theorem\nprover l
 ooking at its capabilities and applications to modern\nmathematics. Finall
 y\, we will turn to the formal development of Turing\nreducibility\, equiv
 alence\, and the induced degrees defined as a\nquotient. The goal is to de
 monstrate both how classical computability\ntheory can be mechanized in Le
 an and how the resulting framework\nsupports further formalization in logi
 c and computable structure\ntheory.\n\nMC 5403
DTSTAMP:20260502T041554Z
END:VEVENT
END:VCALENDAR