BEGIN:VCALENDAR VERSION:2.0 PRODID:researchseminars.org CALSCALE:GREGORIAN X-WR-CALNAME:researchseminars.org BEGIN:VEVENT SUMMARY:Jonathan Sterling DTSTART:20230928T170000Z DTEND:20230928T180000Z DTSTAMP:20260909T071514Z UID:ToposInstituteColloquium/105 DESCRIPTION:Title: Synthetic Domains in the 21st Century\nby Jonathan Sterling as part of Topos Institute Colloquium\n\n\nAbstract\nIt is easy t o teach a student how to give a naïve denotational semantics to a typed l ambda calculus without recursion\, and then use it to reason about the equ ational theory: a type might as well be a set\, and a program might as wel l be a function\, and equational adequacy at base type is established usin g a logical relation between the initial model and the category of sets. A dding any non-trivial feature to this language (e.g. general recursion\, p olymorphism\, state\, etc.) immediately increases the difficulty beyond th e facility of a beginner: to add recursion\, one must replace sets and fun ctions with domains and continuous maps\, and to accommodate polymorphism and state\, one must pass to increasingly inaccessible variations on this basic picture.\n\nThe dream of the 1990s was to find a category that behav es like SET in which even general recursive and effectful programming lang uages could be given naïve denotational semantics\, where types are inter preted as “sets” and programs are interpreted as a “functions”\, w ithout needing to check any arduous technical conditions like continuity. The benefit of this synthetic domain theory is not only that it looks “e asy” for beginners\, as more expert-level constructions like powerdomain s or even domain equations for recursively defined semantic worlds become simple and direct. Although there have been starts and stops\, the dream o f synthetic domain theory is alive and well in the 21st Century. Today’s synthetic domain theory is\, however\, both more modular and more powerfu l than ever before\, and has yielded significant results in programming la nguage semantics including simple denotational semantics for an state of t he art programming language with higher-order polymorphism\, dependent typ es\, recursive types\, general reference types\, and first-class module pa ckages that can be stored in the heap.\n\nIn this talk\, I will explain so me important classical results in synthetic domain theory as well as more recent results that illustrate the potential impact of “naïve denotatio nal semantics” on the life of a workaday computer scientist.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/105/ END:VEVENT END:VCALENDAR