University of Cambridge > > Category Theory Seminar > Categorical Models of Explicit Substitutions

Categorical Models of Explicit Substitutions

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

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:

This talk is part of the Category Theory Seminar series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2023, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity