BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Harry Goldstein (University at Buffalo\, SUNY)
DTSTART:20260120T170000Z
DTEND:20260120T173000Z
DTSTAMP:20260420T025212Z
UID:LT2026/20
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/20/">
 Metaprogramming the Next Generation of Testing Tools</a>\nby Harry Goldste
 in (University at Buffalo\, SUNY) as part of Lean Together 2026\n\n\nAbstr
 act\nLean is an incredible platform for mathematics\, but it is also an ex
 tremely capable programming language. By combining dependent types with a 
 state-of-the-art metaprogramming system\, Lean enables new approaches to w
 riting everyday programs.\n\nIn this talk\, I describe work that my collea
 gues and I have done over the last year that uses metaprogramming in Lean 
 to build new tools for automated testing. I'll demonstrate how Lean's proo
 f system can be repurposed as a system for interactive program synthesis\,
  and I'll show off some other interactive programming interfaces that woul
 d require far more work to implement in other languages.\n\nI hope that my
  talk will provide a glimpse of a new generation of testing tools and insp
 ire others to consider the expressive power of Lean in other programming d
 omains.\n
LOCATION:https://researchseminars.org/talk/LT2026/20/
END:VEVENT
END:VCALENDAR