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...
Saved in:
Published in: | Mathematical structures in computer science 2018-08, Vol.28 (7), p.1061-1096 |
---|---|
Main Authors: | , |
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!
|
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 |