COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Excuse My Extrusion

## Excuse My ExtrusionAdd to your list(s) Download to your calendar using vCal - Conor McBride, Mathematically Structured Programming Group, Department of Computer and Information Sciences, the University of Strathclyde
- Friday 19 February 2016, 14:00-15:00
- FW26.
If you have a question about this talk, please contact Ohad Kammar. Writing this in mid-December, I can promise only a classical tale of triumph or disaster which I hope to have made constructive by mid-February. I have recently begun to learn about the Cubical Type Theory of Coquand et al., as an effective computational basis for Voevodsky’s Univalent Foundations, inspired by a model of type theory in cubical sets. It is in some ways compelling in its simplicity, but in other ways intimidating in its complexity. In order to get to grips with it, I have begun to develop my own much less subtle variation on the theme. If I am lucky, I shall get away with it. If I am unlucky, I shall have learned more about why Cubical Type Theory has to be as subtle as it is. My design separates Coquand’s all-powerful “compose” operator into smaller pieces, dedicated to more specific tasks, such as transitivity of paths. Each type path Q : S = T, induces a notion of value path s {Q} t, where either s : S, or s is •, “blob”, and similarly, t : T or t = •. A “blob” at one end indicates that the value at that end of the path is not mandated by the type. This liberalisation in the formation of “equality” types allows us to specify the key computational use of paths between types, extrusion: if Q : S = T and s : S, then s That is, whenever we have a value s at one end of a type path Q : S = T, we can extrude that value across the type path, getting a value path which is s at the S end, but whose value at the T end is not specified in advance of explaining how to compute it. Extrusion gives us a notion of coercion-by-equality which is coherent by construction. It is defined by recursion on the structure of type paths. Univalence can be added to the system by allowing the formation of types interpolating two equivalent types, with extrusion demanding the existence of the corresponding interpolant values, computed on demand by means of the equivalence. So far, there are disconcerting grounds for optimism, but the whole of the picture has not yet emerged: I may just have pushed the essential complexity into one corner, or the whole thing may be holed below the waterline. But if it does turn out to be nonsense, it will be nonsense for an interesting reason. This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series. ## This talk is included in these lists:- All Talks (aka the CURE list)
- Cambridge talks
- Computer Laboratory talks
- Computing and Mathematics
- FW26
- Interested Talks
- Logic and Semantics Seminar (Computer Laboratory)
- School of Technology
- Trust & Technology Initiative - interesting events
- bld31
- yk373's list
Note that ex-directory lists are not shown. |
## Other listsBiology talks Pragmatics reading group Finance - Centre for Financial Research## Other talksIntroduction to the early detection of cancer and novel interventions Adding turbulent convection to geostrophic circulation: insights into ocean heat transport Propaganda porcelain: The mirror of the Russian revolution and its consequences Hypergraph Saturation Irregularities Replication or exploration? Sequential design for stochastic simulation experiments |