BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Sebastian Ullrich (Lean FRO)
DTSTART:20260120T143000Z
DTEND:20260120T150000Z
DTSTAMP:20260420T025840Z
UID:LT2026/15
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/15/">
 The Lean module system</a>\nby Sebastian Ullrich (Lean FRO) as part of Lea
 n Together 2026\n\n\nAbstract\nThe module system is a new extension of the
  Lean language that allows for more control over the public interface of L
 ean files\, considerably increasing robustness and scalability of librarie
 s in multiple aspects. In this talk\, I will cover the basics of the modul
 e system and what impact we are already seeing from its adoption in Mathli
 b and beyond.\n\nMore info:\n* https://lean-lang.org/doc/reference/latest/
 Source-Files-and-Modules/#module-scopes\n* https://drive.google.com/file/d
 /1AyaYBwnYON_bq3aWjS-Nr3b4vne7c4SJ/view ("Optimizing Lean Libraries using 
 the Module System" starts at 1:06:25)\n
LOCATION:https://researchseminars.org/talk/LT2026/15/
END:VEVENT
END:VCALENDAR