Transport of finiteness structures and applications
Logic in Computer Science
2016-12-15 v2 Logic
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.
Cite
@article{arxiv.1004.3655,
title = {Transport of finiteness structures and applications},
author = {Christine Tasson and Lionel Vaux},
journal= {arXiv preprint arXiv:1004.3655},
year = {2016}
}