BEGIN:VCALENDAR VERSION:2.0 PRODID:researchseminars.org CALSCALE:GREGORIAN X-WR-CALNAME:researchseminars.org BEGIN:VEVENT SUMMARY:Shaowei Lin DTSTART:20250530T153000Z DTEND:20250530T163000Z DTSTAMP:20260422T171811Z UID:CompMath/14 DESCRIPTION:Title: Refine yourself a code for great good!\nby Shaowei Lin as part of Re latorium seminar\n\n\nAbstract\nHow do you code? Andrej Karpathy who coine d the term "vibe coding\," says that for professional coding tasks\, he pi cks single concrete incremental changes and\, with AI assistance\, plans t hem\, executes them\, and evaluates them. Refinement is the process of mak ing incremental changes. It is not just the primary way we design and cons truct code\, but also how we repair them and upgrade them\, often collabor atively with other coders\, designers and users.\n\nThe central objects in refinement are partially implemented programs. Partial programs are examp les of open systems - each has a formal external specification (e.g. a fun ction type) and an implementation with internal holes which are also forma lly specified. Partial proofs\, such as those manipulated by the proof ass istants\, are also examples of open systems. Open systems compose by refin ement or hole-filling\, where a typed hole can only be filled by an open s ystem of the right spec. An open system in some representation can also be translated (transported\, projected or lifted) to some open system in ano ther representation. In fact\, open systems\, with their refinements and t ranslations\, form a double category!\n\nIn this talk\, I hope to share so me concrete examples of this refinement-centric approach in formal verific ation\, program synthesis and theorem proving. I believe that this approac h can help us to leverage AI assistance in coding\, to decentralize and de mocratize coding\, and to build safe\, secure and sustainable software sys tems.\n\nModerator: The talk will be moderated by Daniel Filonik. Daniel s pecializes in data visualization and human computer interaction. His recen t work focused on natural interfaces for interactive data modeling and ana lysis with formal foundations in category theory.\n LOCATION:https://researchseminars.org/talk/CompMath/14/ END:VEVENT END:VCALENDAR