Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

TLCA

2009

Springer

2009

Springer

Finiteness spaces constitute a categorical model of Linear Logic whose objects can be seen as linearly topologised spaces, (a class of topological vector spaces introduced by Lefschetz in 1942) and morphisms as continuous linear maps. First, we recall deﬁnitions of ﬁniteness spaces and describe their basic properties deduced from the general theory of linearly topologised spaces. Then we give the interpretation of LL with an algebraic approach. Second, thanks to separation properties, we can introduce an algebraic notion of totality candidate in the framework of linearly topologised spaces: a totality candidate is a closed afﬁne subspace which does not contain 0. We show that ﬁniteness spaces with totality candidates constitute a model of classical LL. Finally, we give a barycentric simply typed lambda-calculus, with booleans B and a conditional operator, which can be interpreted in this model. We prove completeness at type Bn → B for every n by an algebraic method.

Related Content

Added |
27 May 2010 |

Updated |
27 May 2010 |

Type |
Conference |

Year |
2009 |

Where |
TLCA |

Authors |
Christine Tasson |

Comments (0)