Abstract

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