BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Sebastian Graf (Lean FRO)
DTSTART:20260120T160000Z
DTEND:20260120T163000Z
DTSTAMP:20260420T025808Z
UID:LT2026/18
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/18/">
 Simpler $\\texttt{do}$ proofs with $\\texttt{mvcgen}$</a>\nby Sebastian Gr
 af (Lean FRO) as part of Lean Together 2026\n\n\nAbstract\nSince last year
 \, $\\texttt{Std}$ features $\\texttt{mvcgen}$\, a new experimental tactic
  that implements a monadic verification condition generator. It breaks dow
 n a goal involving a program written using Lean's imperative $\\texttt{do}
 $ notation into a number of smaller $\\textit{verification conditions}$ th
 at are sufficient to prove the goal.\n\nIn this talk\, we will go through 
 a couple of examples that show how $\\texttt{mvcgen}$ enables compositiona
 l reasoning where previous tactics fall short and have a look at its seman
 tic foundations.\n
LOCATION:https://researchseminars.org/talk/LT2026/18/
END:VEVENT
END:VCALENDAR