BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Chris Henson (Drexel University)
DTSTART:20260121T203000Z
DTEND:20260121T210000Z
DTSTAMP:20260420T025149Z
UID:LT2026/30
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/30/">
 Proof Automation and Metaprogramming in CSLib: Locally Nameless Lambda Cal
 culi</a>\nby Chris Henson (Drexel University) as part of Lean Together 202
 6\n\n\nAbstract\nThis talk will discuss CSLib's locally nameless formaliza
 tion of lambda calculi\, which currently includes STLC and System F with s
 ubtyping. While this is a well-established style of formalization\, we use
  Lean's new proof automation features and metaprogramming in ways that are
  interesting to consider. We make heavy use of the grind tactic\, allowing
  us to easily reuse existing Mathlib infrastructure for typing contexts an
 d in general enable a succinct style that is approximately 45% fewer LoC t
 han comparable formalizations. Metaprogramming has also been useful\, allo
 wing us to standardize certain notations and develop a single term elabora
 tor for selecting fresh variables that does not require specialization for
  each type system.\n
LOCATION:https://researchseminars.org/talk/LT2026/30/
END:VEVENT
END:VCALENDAR