BEGIN:VCALENDAR VERSION:2.0 PRODID:researchseminars.org CALSCALE:GREGORIAN X-WR-CALNAME:researchseminars.org BEGIN:VEVENT SUMMARY:Robert Harper DTSTART:20211209T170000Z DTEND:20211209T180000Z DTSTAMP:20260406T164933Z UID:ToposInstituteColloquium/36 DESCRIPTION:Title: Phase Distinctions in Type Theory\nby Robert Harper as part of Topos Institute Colloquium\n\n\nAbstract\n(Joint work with Jon Sterling and Yue Niu)\n\nThe informal phase distinction between compile-ti me and run-time in programming languages is formally manifested by the dis tinction between kinds\, which classify types\, and types\, which classify code. The distinction underpins standard programming methodology whereby code is first type-checked for consistency before being compiled for execu tion. When used effectively\, types help eliminate bugs before they occur. \n\nProgram modules\, in even the most rudimentary form\, threaten the dis tinction\, comprising as they do both types and programs in a single unit. Matters worsen when considerating "open" modules\, with free module varia bles standing for its imports. To maintain the separation in their presenc e it is necessary to limit the dependency of types\, the static parts of a module\, to their imported types. Such restrictions are fundamental for u sing dependent types to express modular structure\, as originally suggeste d by MacQueen.\n\nTo address this question Moggi gave an "analytic" formul ation of program modules in which modules are explicitly separated into th eir static and dynamic components using tools from category theory. Recent work by Dreyer\, Rossberg\, and Russo develops this approach fully in the ir account of ML-like module systems. In this talk we consider instead a " synthetic" formulation using a proposition to segregate the static from th e dynamic\, in particular to define static equivalence to manage type shar ing and type dependency\n\nRobert Harper is a Professor of Computer Scienc e at Carnegie Mellon\, where he\nhas been a member of faculty since 1988. He is past recipient of the Allen\nNewell Award for research excellence an d the Herbert Simon Award for teaching\nexcellence. He is author of Practi cal Foundations for Programming Languages\, a\ntextbook account of program ming language theory. His work focuses on the\napplication of type theory to program development\, language design\, compiler\nconstruction\, and m echanized proof.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/36/ END:VEVENT END:VCALENDAR