Categorical Models of Explicit Substitutions

Add to your list(s) Download to your calendar using vCal

• Valeria de Paiva (Topos Institute)
• Tuesday 01 June 2021, 16:15-17:15
• Zoom (Meeting ID 996 6732 5570, passcode 109362).

If you have a question about this talk, please contact José Siqueira.

The advantages of functional programming are well-known: programs are easier to write, understand and verify than their imperative counterparts. However, functional languages tend to be more memory intensive and these problems have hindered their wider use in industry. The xSLAM project tried to address these issues by using explicit substitutions to construct and implement more efficient abstract machines. In this work we provide categorical models for the calculi of explicit substitutions (linear and cartesian) that we are interested in.

Indexed categories provide models of cartesian calculi of explicit substitutions. However, these structures are inherently non-linear and hence cannot be used to model linear calculi of explicit substitutions. This work replaces indexed categories with pre-sheaves, thus providing a categorical semantics covering both the linear and cartesian cases. We justify our models by proving soundness and completeness results. Then we speculate on why there are not many models around, given the large number of calculi discussed in the community.

Zoom link: https://maths-cam-ac-uk.zoom.us/j/99667325570?pwd=TC9RakFUcGZQdEM5bExMbzlraDZOZz09

This talk is part of the Category Theory Seminar series.

This talk is included in these lists:

• All CMS events
• All Talks (aka the CURE list)
• CMS Events
• Category Theory Seminar
• DPMMS Lists
• DPMMS Pure Maths Seminar
• DPMMS info aggregator
• DPMMS lists
• Hanchen DaDaDash
• Interested Talks
• School of Physical Sciences
• Zoom (Meeting ID 996 6732 5570, passcode 109362)
• bld31
• ndb35's list
• yk373's list

Note that ex-directory lists are not shown.