| Issue |
RAIRO-Theor. Inf. Appl.
Volume 47, Number 1, January-March 2013
6th Workshop on Fixed Points in Computer Science (FICS'09)
|
|
|---|---|---|
| Page(s) | 111 - 132 | |
| DOI | https://doi.org/10.1051/ita/2012031 | |
| Published online | 10 January 2013 | |
A non-uniform finitary relational semantics of system T∗
Institut de Mathématiques de Luminy (IML), Aix-Marseille
Université, 163 avenue de Luminy,
Case 907, 13288
Marseille Cedex 9,
France.
vaux@iml.univ-mrs.fr
Received:
28
September
2012
Accepted:
28
September
2012
We study iteration and recursion operators in the denotational semantics of typed λ-calculi derived from the multiset relational model of linear logic. Although these operators are defined as fixpoints of typed functionals, we prove them finitary in the sense of Ehrhard’s finiteness spaces.
Mathematics Subject Classification: 03B70 / 03D65 / 68Q55
Key words: Higher order primitive recursion / denotational semantics
© EDP Sciences 2013
Current usage metrics show cumulative count of Article Views (full-text article views including HTML views, PDF and ePub downloads, according to the available data) and Abstracts Views on Vision4Press platform.
Data correspond to usage on the plateform after 2015. The current usage metrics is available 48-96 hours after online publication and is updated daily on week days.
Initial download of the metrics may take a while.