Loading…

Transport of finiteness structures and applications

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...

Full description

Saved in:
Bibliographic Details
Published in:Mathematical structures in computer science 2018-08, Vol.28 (7), p.1061-1096
Main Authors: TASSON, CHRISTINE, VAUX, LIONEL
Format: Article
Language:English
Subjects:
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0960-1295
1469-8072
DOI:10.1017/S0960129516000384