BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//jEvents 2.0 for Joomla//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
BEGIN:VTIMEZONE
TZID:America/New_York
BEGIN:STANDARD
DTSTART:20250303T100000
RDATE:20250309T030000
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:America/New_York EST
END:STANDARD
BEGIN:STANDARD
DTSTART:20251102T010000
RDATE:20260308T030000
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:America/New_York EST
END:STANDARD
BEGIN:STANDARD
DTSTART:20261101T010000
RDATE:20270314T030000
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:America/New_York EST
END:STANDARD
BEGIN:STANDARD
DTSTART:20271107T010000
RDATE:20280312T030000
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:America/New_York EST
END:STANDARD
BEGIN:STANDARD
DTSTART:20281105T010000
RDATE:20290311T030000
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:America/New_York EST
END:STANDARD
BEGIN:DAYLIGHT
DTSTART:20250309T030000
RDATE:20251102T010000
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:America/New_York EDT
END:DAYLIGHT
BEGIN:DAYLIGHT
DTSTART:20260308T030000
RDATE:20261101T010000
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:America/New_York EDT
END:DAYLIGHT
BEGIN:DAYLIGHT
DTSTART:20270314T030000
RDATE:20271107T010000
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:America/New_York EDT
END:DAYLIGHT
BEGIN:DAYLIGHT
DTSTART:20280312T030000
RDATE:20281105T010000
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:America/New_York EDT
END:DAYLIGHT
END:VTIMEZONE
BEGIN:VEVENT
UID:0b9b3e4fe8f9de1fe167d4d12d8c98d0
CATEGORIES:Lean Seminar
CREATED:20260227T211101
SUMMARY:Designing Interactive Partners for Proof
LOCATION:Hill 705
DESCRIPTION:<p><span style="color: #242424; font-family: 'Segoe UI', 'Segoe UI Web (Wes
 t European)', -apple-system, 'system-ui', Roboto, 'Helvetica Neue', sans-se
 rif; font-size: 15px; font-style: normal; font-weight: 400; letter-spacing:
  normal; orphans: 2; text-align: start; text-indent: 0px; text-transform: n
 one; widows: 2; word-spacing: 0px; white-space: normal; background-color: #
 ffffff; float: none;">Whenever someone builds a sufficiently complex system
 , they need to check that it does what they intend. Some aspects of system 
 behavior are so important that their developers write&nbsp;</span><span sty
 le="border: 0px; font-style: normal; font-weight: 400; font-size: 15px; lin
 e-height: inherit; font-family: 'Segoe UI', 'Segoe UI Web (West European)',
  -apple-system, 'system-ui', Roboto, 'Helvetica Neue', sans-serif; margin: 
 0px; padding: 0px; vertical-align: baseline; color: #242424; letter-spacing
 : normal; orphans: 2; text-align: start; text-indent: 0px; text-transform: 
 none; widows: 2; word-spacing: 0px; white-space: normal; background-color: 
 #ffffff;">proofs</span><span style="color: #242424; font-family: 'Segoe UI'
 , 'Segoe UI Web (West European)', -apple-system, 'system-ui', Roboto, 'Helv
 etica Neue', sans-serif; font-size: 15px; font-style: normal; font-weight: 
 400; letter-spacing: normal; orphans: 2; text-align: start; text-indent: 0p
 x; text-transform: none; widows: 2; word-spacing: 0px; white-space: normal;
  background-color: #ffffff; float: none;">&nbsp;to show that they are corre
 ct. This kind of&nbsp;</span><span style="border: 0px; font-style: normal; 
 font-weight: 400; font-size: 15px; line-height: inherit; font-family: 'Sego
 e UI', 'Segoe UI Web (West European)', -apple-system, 'system-ui', Roboto, 
 'Helvetica Neue', sans-serif; margin: 0px; padding: 0px; vertical-align: ba
 seline; color: #242424; letter-spacing: normal; orphans: 2; text-align: sta
 rt; text-indent: 0px; text-transform: none; widows: 2; word-spacing: 0px; w
 hite-space: normal; background-color: #ffffff;">proof</span><span style="co
 lor: #242424; font-family: 'Segoe UI', 'Segoe UI Web (West European)', -app
 le-system, 'system-ui', Roboto, 'Helvetica Neue', sans-serif; font-size: 15
 px; font-style: normal; font-weight: 400; letter-spacing: normal; orphans: 
 2; text-align: start; text-indent: 0px; text-transform: none; widows: 2; wo
 rd-spacing: 0px; white-space: normal; background-color: #ffffff; float: non
 e;">&nbsp;work can be essential. But it is also grueling. Could we give peo
 ple better tools to establish soundness of systems and understand the forma
 lisms that model them? In this talk, I share a modern vision for user inter
 faces that serve as&nbsp;</span><span style="border: 0px; font-style: norma
 l; font-weight: 400; font-size: 15px; line-height: inherit; font-family: 'S
 egoe UI', 'Segoe UI Web (West European)', -apple-system, 'system-ui', Robot
 o, 'Helvetica Neue', sans-serif; margin: 0px; padding: 0px; vertical-align:
  baseline; color: #242424; letter-spacing: normal; orphans: 2; text-align: 
 start; text-indent: 0px; text-transform: none; widows: 2; word-spacing: 0px
 ; white-space: normal; background-color: #ffffff;">partners</span><span sty
 le="color: #242424; font-family: 'Segoe UI', 'Segoe UI Web (West European)'
 , -apple-system, 'system-ui', Roboto, 'Helvetica Neue', sans-serif; font-si
 ze: 15px; font-style: normal; font-weight: 400; letter-spacing: normal; orp
 hans: 2; text-align: start; text-indent: 0px; text-transform: none; widows:
  2; word-spacing: 0px; white-space: normal; background-color: #ffffff; floa
 t: none;">&nbsp;in making and understanding&nbsp;</span><span style="border
 : 0px; font-style: normal; font-weight: 400; font-size: 15px; line-height: 
 inherit; font-family: 'Segoe UI', 'Segoe UI Web (West European)', -apple-sy
 stem, 'system-ui', Roboto, 'Helvetica Neue', sans-serif; margin: 0px; paddi
 ng: 0px; vertical-align: baseline; color: #242424; letter-spacing: normal; 
 orphans: 2; text-align: start; text-indent: 0px; text-transform: none; wido
 ws: 2; word-spacing: 0px; white-space: normal; background-color: #ffffff;">
 proof</span><span style="color: #242424; font-family: 'Segoe UI', 'Segoe UI
  Web (West European)', -apple-system, 'system-ui', Roboto, 'Helvetica Neue'
 , sans-serif; font-size: 15px; font-style: normal; font-weight: 400; letter
 -spacing: normal; orphans: 2; text-align: start; text-indent: 0px; text-tra
 nsform: none; widows: 2; word-spacing: 0px; white-space: normal; background
 -color: #ffffff; float: none;">. The foundation is recent research from my 
 group on the usage of modern&nbsp;</span><span style="border: 0px; font-sty
 le: normal; font-weight: 400; font-size: 15px; line-height: inherit; font-f
 amily: 'Segoe UI', 'Segoe UI Web (West European)', -apple-system, 'system-u
 i', Roboto, 'Helvetica Neue', sans-serif; margin: 0px; padding: 0px; vertic
 al-align: baseline; color: #242424; letter-spacing: normal; orphans: 2; tex
 t-align: start; text-indent: 0px; text-transform: none; widows: 2; word-spa
 cing: 0px; white-space: normal; background-color: #ffffff;">proof</span><sp
 an style="color: #242424; font-family: 'Segoe UI', 'Segoe UI Web (West Euro
 pean)', -apple-system, 'system-ui', Roboto, 'Helvetica Neue', sans-serif; f
 ont-size: 15px; font-style: normal; font-weight: 400; letter-spacing: norma
 l; orphans: 2; text-align: start; text-indent: 0px; text-transform: none; w
 idows: 2; word-spacing: 0px; white-space: normal; background-color: #ffffff
 ; float: none;">&nbsp;assistants. The building blocks are a set of prototyp
 e&nbsp;</span><span style="border: 0px; font-style: normal; font-weight: 40
 0; font-size: 15px; line-height: inherit; font-family: 'Segoe UI', 'Segoe U
 I Web (West European)', -apple-system, 'system-ui', Roboto, 'Helvetica Neue
 ', sans-serif; margin: 0px; padding: 0px; vertical-align: baseline; color: 
 #242424; letter-spacing: normal; orphans: 2; text-align: start; text-indent
 : 0px; text-transform: none; widows: 2; word-spacing: 0px; white-space: nor
 mal; background-color: #ffffff;">interactive</span><span style="color: #242
 424; font-family: 'Segoe UI', 'Segoe UI Web (West European)', -apple-system
 , 'system-ui', Roboto, 'Helvetica Neue', sans-serif; font-size: 15px; font-
 style: normal; font-weight: 400; letter-spacing: normal; orphans: 2; text-a
 lign: start; text-indent: 0px; text-transform: none; widows: 2; word-spacin
 g: 0px; white-space: normal; background-color: #ffffff; float: none;">&nbsp
 ;systems we have developed for automated testing, math authoring, and progr
 am QA. Together, these components help to outline how future&nbsp;</span><s
 pan style="border: 0px; font-style: normal; font-weight: 400; font-size: 15
 px; line-height: inherit; font-family: 'Segoe UI', 'Segoe UI Web (West Euro
 pean)', -apple-system, 'system-ui', Roboto, 'Helvetica Neue', sans-serif; m
 argin: 0px; padding: 0px; vertical-align: baseline; color: #242424; letter-
 spacing: normal; orphans: 2; text-align: start; text-indent: 0px; text-tran
 sform: none; widows: 2; word-spacing: 0px; white-space: normal; background-
 color: #ffffff;">proof</span><span style="color: #242424; font-family: 'Seg
 oe UI', 'Segoe UI Web (West European)', -apple-system, 'system-ui', Roboto,
  'Helvetica Neue', sans-serif; font-size: 15px; font-style: normal; font-we
 ight: 400; letter-spacing: normal; orphans: 2; text-align: start; text-inde
 nt: 0px; text-transform: none; widows: 2; word-spacing: 0px; white-space: n
 ormal; background-color: #ffffff; float: none;">&nbsp;tools can assist in c
 hecking complex systems and understanding the formalisms they draw on.</spa
 n></p>
CONTACT:Andrew Head
DTSTAMP:20260827T155933
DTSTART;TZID=America/New_York:20260304T100000
DTEND;TZID=America/New_York:20260304T110000
SEQUENCE:0
TRANSP:OPAQUE
END:VEVENT
END:VCALENDAR