Finiteness spaces Export

@article{citeulike:5990590, abstract = {We investigate a new denotational model of linear logic based on the purely relational model. In this semantics, webs are equipped with a notion of \‘finitary\’ subsets satisfying a closure condition and proofs are interpreted as finitary sets. In spite of a formal similarity, this model is quite different from the usual models of linear logic (coherence semantics, hypercoherence semantics, the various existing game semantics\…). In particular, the standard fix-point operators used for defining the general recursive functions are not finitary, although the primitive recursion operators are. This model can be considered as a discrete analogue of the K\öthe space semantics introduced in a previous paper: we show how, given a field, each finiteness space gives rise to a vector space endowed with a linear topology , a notion introduced by Lefschetz in 1942, and we study the corresponding model where morphisms are linear continuous maps (a version of Girard's quantitative semantics with coefficients in the field). In this way we obtain a new model of the recently introduced differential lambda-calculus .}, address = {New York, NY, USA}, author = {Ehrhard, Thomas}, citeulike-article-id = {5990590}, citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=1089906}, citeulike-linkout-1 = {http://dx.doi.org/10.1017/S0960129504004645}, citeulike-linkout-2 = {http://www.pps.jussieu.fr/~ehrhard/pub/finite.pdf}, doi = {10.1017/S0960129504004645}, issn = {0960-1295}, journal = {Mathematical. Structures in Comp. Sci.}, keywords = {denotational\_semantics, linear\_logic}, number = {4}, pages = {615--646}, posted-at = {2009-10-23 00:31:08}, priority = {4}, publisher = {Cambridge University Press}, title = {Finiteness spaces}, url = {http://dx.doi.org/10.1017/S0960129504004645}, volume = {15}, year = {2005} }

TY - JOUR ID - citeulike:5990590 L3 - citeulike-article-id:5990590 N2 - We investigate a new denotational model of linear logic based on the purely relational model. In this semantics, webs are equipped with a notion of ‘finitary’ subsets satisfying a closure condition and proofs are interpreted as finitary sets. In spite of a formal similarity, this model is quite different from the usual models of linear logic (coherence semantics, hypercoherence semantics, the various existing game semantics…). In particular, the standard fix-point operators used for defining the general recursive functions are not finitary, although the primitive recursion operators are. This model can be considered as a discrete analogue of the Köthe space semantics introduced in a previous paper: we show how, given a field, each finiteness space gives rise to a vector space endowed with a linear topology , a notion introduced by Lefschetz in 1942, and we study the corresponding model where morphisms are linear continuous maps (a version of Girard's quantitative semantics with coefficients in the field). In this way we obtain a new model of the recently introduced differential lambda-calculus . IS - 4 JF - Mathematical. Structures in Comp. Sci. SN - 0960-1295 AD - New York, NY, USA EP - 646 TI - Finiteness spaces PB - Cambridge University Press VL - 15 SP - 615 KW - denotational_semantics KW - linear_logic AU - Ehrhard, Thomas PY - 2005/// UR - http://dx.doi.org/10.1017/S0960129504004645 ER -