Transport of finiteness structures and applications

TL;DR

This paper introduces a general construction of finiteness spaces that encompasses all positive connectors of linear logic and demonstrates how to establish least fixpoints for certain functors within this framework.

Contribution

It presents a unified construction of finiteness spaces and applies it to prove the existence of least fixpoints for functors related to recursive algebraic datatypes.

Findings

Unified construction of finiteness spaces for linear logic

Existence of least fixpoints for specific functors in finiteness spaces

Application to semantics of recursive algebraic datatypes

Abstract

We describe a general construction of finiteness spaces which subsumes the interpretations of all positive connectors of linear logic. We then show how to apply this construction to prove the existence of least fixpoints for particular functors in the category of finiteness spaces: these include the functors involved in a relational interpretation of lazy recursive algebraic datatypes along the lines of the coherence semantics of system T.