Events and news relevant to the Laboratory for Foundations of Computer Science

[Paul Jackson <Paul.Jackson@ed.ac.uk>]

BEGIN:VCALENDAR
METHOD:REQUEST
PRODID:Microsoft Exchange Server 2010
VERSION:2.0
BEGIN:VTIMEZONE
TZID:GMT Standard Time
BEGIN:STANDARD
DTSTART:16010101T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
RRULE:FREQ=YEARLY;INTERVAL=1;BYDAY=-1SU;BYMONTH=10
END:STANDARD
BEGIN:DAYLIGHT
DTSTART:16010101T010000
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
RRULE:FREQ=YEARLY;INTERVAL=1;BYDAY=-1SU;BYMONTH=3
END:DAYLIGHT
END:VTIMEZONE
BEGIN:VEVENT
ORGANIZER;CN=Paul Jackson:mailto:Paul.Jackson@ed.ac.uk
ATTENDEE;ROLE=REQ-PARTICIPANT;PARTSTAT=NEEDS-ACTION;RSVP=TRUE;CN=AIAI Membe
 rs:mailto:aiai-members@inf.ed.ac.uk
ATTENDEE;ROLE=REQ-PARTICIPANT;PARTSTAT=NEEDS-ACTION;RSVP=TRUE;CN=LFCS Inter
 est:mailto:lfcs-interest@mlist.is.ed.ac.uk
ATTENDEE;ROLE=REQ-PARTICIPANT;PARTSTAT=NEEDS-ACTION;RSVP=TRUE;CN=inf-dreame
 rs@mlist.is.ed.ac.uk:mailto:inf-dreamers@mlist.is.ed.ac.uk
DESCRIPTION;LANGUAGE=en-GB:Hi\,\n4-5pm Tuesday 21st July  in IF 3.02 and on
 line\, Aeacus Sheng and Alex Hyman will give practice runs of their Isabel
 le-related FLoC talks:\n\n\n  *\nAeacus Sheng: Faster Verified Real Root I
 solation with Descartes' Rule of Signs\n  *\nAlex Hyman: IsaGrad: Verified
  Automatic Differentiation over Computational Graphs in Imperative HOL\n\n
 Further details below.\n\nFeedback will be welcome!\n\nBest wishes\,\nPaul
 .\n\n\nAeacus Sheng\, Wenda Li and Paul Jackson.\nFaster Verified Real Roo
 t Isolation with Descartes' Rule of Signs.\n\nAt ITP: https://itp-conferen
 ce-2026.github.io/.\n\nReal root isolation is a fundamental subroutine in 
 computer algebra\, with applications ranging from algebraic number arithme
 tic to solving polynomial systems. Modern implementations typically employ
  subdivision methods based on root counting via Descartes' rule of signs. 
 In contrast\, most existing formally verified root isolation procedures re
 ly on Sturm's theorem for root counting\, leading to a noticeable gap betw
 een practical implementations and formally verified approaches.\nWe take a
 n initial step towards efficient verified real root isolation by formally 
 verifying two simple algorithms based on Descartes' rule of signs: a class
 ical bisection procedure and a Newton-accelerated variant. In this paper\,
  we describe the algorithms\, present formal proofs of termination\, sound
 ness\, and completeness\, and discuss our code-generation efforts. Brief e
 xperiments show promising performance improvements over existing formally 
 verified algorithms in Isabelle/HOL.\nhttps://drops.dagstuhl.de/entities/d
 ocument/10.4230/LIPIcs.ITP.2026.32\n\n\nAlex Hyman\, Filip Smola\, Mark Ch
 evallier and Jacques Fleuriot.\nIsaGrad: Verified Automatic Differentiatio
 n over Computational Graphs in Imperative HOL\n\nAt LogicNN: https://perso
 .ens-lyon.fr/francois.schwarzentruber/research/events/logicnn2026/.\n\nWe 
 present IsaGrad\, a formalisation of scalar reverse automatic differentiat
 ion (RAD) over mutable reference-\nbased computational graphs using the Im
 perative HOL library of Isabelle\, and verify its functional correctness b
 y\nan interactive separation-logic proof. We use IsaGrad as the differenti
 ation engine for two machine learning case\nstudies: training a multi-laye
 r perceptron and a recurrent neural network. Leveraging Isabelle’s code 
 generation\,\nwe extract imperative-style Haskell programs where the train
 ing process is backed by our verified algorithm. To\nour knowledge\, our i
 mplementation is the first of its kind to prove the functional correctness
  of an imperative\,\nheap-based RAD algorithm. Beyond showcasing Imperativ
 e HOL’s expressiveness\, this work demonstrates how\nformal verification
  increases confidence in computational graphs used for gradient-based opti
 misation\, including\nneural network training.\n\n\n\n\n__________________
 ______________________________________________________________\nMicrosoft 
 Teams meeting\nJoin: https://teams.microsoft.com/meet/391497302667447?p=6G
 SqBf6GkHVANOPklT\nMeeting ID: 391 497 302 667 447\nPasscode: jK6sw7W6\n___
 _____________________________\nNeed help?<https://aka.ms/JoinTeamsMeeting?
 omkt=en-GB> | System reference<https://teams.microsoft.com/l/meetup-join/1
 9%3ameeting_YWE1NTUyYzYtYjU5MC00ODY5LWI0OTItNjY2MzZlNmQ4M2Q4%40thread.v2/0
 ?context=%7b%22Tid%22%3a%222e9f06b0-1669-4589-8789-10a06934dc61%22%2c%22Oi
 d%22%3a%22c578cf5d-b5a8-4979-a6eb-e6d7a0edd3fe%22%7d>\nDial in by phone\n+
 44 20 3855 5143\,\,401050655#<tel:+442038555143\,\,401050655#> United King
 dom\, City of London\nFind a local number<https://dialin.teams.cloud.micro
 soft/41ca4bf1-0212-4fa6-bde8-4d05362d3446?id=401050655>\nPhone conference 
 ID: 401 050 655#\nFor organisers: Meeting options<https://teams.microsoft.
 com/meetingOptions/?organizerId=c578cf5d-b5a8-4979-a6eb-e6d7a0edd3fe&tenan
 tId=2e9f06b0-1669-4589-8789-10a06934dc61&threadId=19_meeting_YWE1NTUyYzYtY
 jU5MC00ODY5LWI0OTItNjY2MzZlNmQ4M2Q4@thread.v2&messageId=0&language=en-GB> 
 | Reset dial-in PIN<https://dialin.teams.cloud.microsoft/usp/pstnconferenc
 ing>\n[https://srvmgmt.is.ed.ac.uk/resources/images/UoELogo-TeamsMeetings.
 jpg]\nThe University of Edinburgh is a charitable body\, registered in Sco
 tland\, with registration number SC005336. Is e buidheann carthannais a th
 ’ ann an Oilthigh Dhùn Èideann\, clàraichte an Alba\, àireamh clàra
 idh SC005336.\nOrg help<https://support.office.com/en-us/article/join-a-me
 eting-in-teams-1613bb53-f3fa-431e-85a9-d6a91e3468c9> | Privacy and securit
 y<https://www.ed.ac.uk/information-services/about/policies-and-regulations
 >\n_______________________________________________________________________
 _________\n
UID:040000008200E00074C5B7101A82E008000000005C2291683D15DD01000000000000000
 010000000466ACC2697013A4B861A2CDDD94F2D6B
SUMMARY;LANGUAGE=en-GB:Isabelle-related FLoC practice talks
DTSTART;TZID=GMT Standard Time:20260721T160000
DTEND;TZID=GMT Standard Time:20260721T170000
CLASS:PUBLIC
PRIORITY:5
DTSTAMP:20260720T082328Z
TRANSP:OPAQUE
STATUS:CONFIRMED
SEQUENCE:0
LOCATION;LANGUAGE=en-GB:IF 3.02
X-MICROSOFT-CDO-APPT-SEQUENCE:0
X-MICROSOFT-CDO-OWNERAPPTID:2124907375
X-MICROSOFT-CDO-BUSYSTATUS:TENTATIVE
X-MICROSOFT-CDO-INTENDEDSTATUS:BUSY
X-MICROSOFT-CDO-ALLDAYEVENT:FALSE
X-MICROSOFT-CDO-IMPORTANCE:1
X-MICROSOFT-CDO-INSTTYPE:0
X-MICROSOFT-ONLINEMEETINGEXTERNALLINK:
X-MICROSOFT-ONLINEMEETINGINFORMATION:{"OnlineMeetingChannelId":null\,"Onlin
 eMeetingProvider":3}
X-MICROSOFT-ONLINEMEETINGTOLLNUMBER:+44 20 3855 5143
X-MICROSOFT-ONLINEMEETINGCONFERENCEID:401050655
X-MICROSOFT-SKYPETEAMSMEETINGURL:https://teams.microsoft.com/l/meetup-join/
 19%3ameeting_YWE1NTUyYzYtYjU5MC00ODY5LWI0OTItNjY2MzZlNmQ4M2Q4%40thread.v2/
 0?context=%7b%22Tid%22%3a%222e9f06b0-1669-4589-8789-10a06934dc61%22%2c%22O
 id%22%3a%22c578cf5d-b5a8-4979-a6eb-e6d7a0edd3fe%22%7d
X-MICROSOFT-SCHEDULINGSERVICEUPDATEURL:https://api.scheduler.teams.microsof
 t.com/teams/2e9f06b0-1669-4589-8789-10a06934dc61/c578cf5d-b5a8-4979-a6eb-e
 6d7a0edd3fe/19_meeting_YWE1NTUyYzYtYjU5MC00ODY5LWI0OTItNjY2MzZlNmQ4M2Q4@th
 read.v2/0
X-MICROSOFT-SKYPETEAMSPROPERTIES:{"cid":"19:meeting_YWE1NTUyYzYtYjU5MC00ODY
 5LWI0OTItNjY2MzZlNmQ4M2Q4@thread.v2"\,"rid":0\,"mid":0\,"uid":null\,"priva
 te":true\,"type":0}
X-MICROSOFT-DONOTFORWARDMEETING:FALSE
X-MICROSOFT-DISALLOW-COUNTER:FALSE
X-MICROSOFT-REQUESTEDATTENDANCEMODE:DEFAULT
X-MICROSOFT-ISRESPONSEREQUESTED:TRUE
X-MICROSOFT-LOCATIONDISPLAYNAME:IF 3.02
X-MICROSOFT-LOCATIONSOURCE:None
X-MICROSOFT-LOCATIONS:[{"DisplayName":"IF 3.02"\,"LocationAnnotation":""\,"
 LocationUri":""\,"LocationStreet":""\,"LocationCity":""\,"LocationState":"
 "\,"LocationCountry":""\,"LocationPostalCode":""\,"LocationFullAddress":""
 }]
BEGIN:VALARM
DESCRIPTION:REMINDER
TRIGGER;RELATED=START:-PT15M
ACTION:DISPLAY
END:VALARM
END:VEVENT
END:VCALENDAR