A non-uniform finitary relational semantics of System T

Lionel Vaux (1)

1 IML - Institut de mathématiques de Luminy

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.

Mots clés: higher order primitive recursion; denotational semantics

Domaines: Logique en informatique [cs.LO]; Logique [math.LO]

Lionel Vaux. A non-uniform finitary relational semantics of System T . RAIRO - Theoretical Informatics and Applications (RAIRO: ITA), 2013, 6th Workshop on Fixed Points in Computer Science (FICS'09), 47 (1), pp.111 - 132. ⟨10.1051/ita/2012031⟩. ⟨hal-01264669⟩