BEGIN:VCALENDAR VERSION:2.0 PRODID:researchseminars.org CALSCALE:GREGORIAN X-WR-CALNAME:researchseminars.org BEGIN:VEVENT SUMMARY:Farzaneh Derakhshan (Carnegie Mellon) DTSTART:20201105T190000Z DTEND:20201105T200000Z DTSTAMP:20260423T035713Z UID:OLS/36 DESCRIPTION:Title: Str ong Progress for Session-Typed Processes in a Linear Metalogic with Circul ar Proofs\nby Farzaneh Derakhshan (Carnegie Mellon) as part of Online logic seminar\n\n\nAbstract\nSession types describe the communication beha vior of interacting processes. Binary session types are a particular form of session types in which each channel has two endpoints. The strong progr ess property states that a recursive process either terminates or communic ates along one of its external channels after a finite number of steps. In this talk\, I show how to prove strong progress for valid session-typed p rocesses defined in an asynchronous computational semantics\, working in a fragment of binary session types in which a process can use at most one r esource. We formalize a proof of strong progress via a processes-as-formul as interpretation into a metalogic that we have introduced. The metalogic is an infinitary first order linear calculus with least and greatest fixed -points. We build a circular derivation for the strong progress property o f processes in this first order calculus. By enforcing a condition on the logical derivations\, we ensure their cut elimination property and soundne ss of the strong progress theorem.\n LOCATION:https://researchseminars.org/talk/OLS/36/ END:VEVENT END:VCALENDAR