An affine-intuitionistic system of types and effects: confluence and termination

Roberto Amadio; Patrick Baillot; Antoine Madet

hal-00438101, version 2

An affine-intuitionistic system of types and effects: confluence and termination

Roberto Amadio () ¹, Patrick Baillot () ², Antoine Madet () ¹

(2010-05-03)

Résumé : We present an affine-intuitionistic system of types and effects which can be regarded as an extension of Barber-Plotkin Dual Intuitionistic Linear Logic to multi-threaded programs with effects. In the system, dynamically generated values such as references or channels are abstracted into a finite set of regions. We introduce a discipline of region usage that entails the confluence (and hence determinacy) of the typable programs. Further, we show that a discipline of region stratification guarantees termination.

1 : Preuves, Programmes et Systèmes (PPS)
CNRS : UMR7126 – Université Paris VII - Paris Diderot
2 : Laboratoire de l'Informatique du Parallélisme (LIP)
Université de Lyon – CNRS : UMR5668 – INRIA – École Normale Supérieure - Lyon – Université Claude Bernard - Lyon I

hal-00438101, version 2
http://hal.archives-ouvertes.fr/hal-00438101
oai:hal.archives-ouvertes.fr:hal-00438101
Contributeur : Roberto Amadio <>
Soumis le : Lundi 3 Mai 2010, 15:56:28
Dernière modification le : Mardi 8 Mai 2012, 13:12:47

Voir la fiche détaillée

Documents associés

PDF :

PS :

arXiv : 1005.0835

Exporter

Bibtex EndNote TEI RefWorks

<?xml version="1.0" encoding="UTF-8"?>
<listBibl xmlns="http://www.tei-c.org/ns/1.0" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:mml="http://www.w3.org/1998/Math/MathML">
<listBibl type="article"><head>Documents sans référence de publication (Preprint)</head>
<biblStruct type="article" xml:id="hal-00438101"><analytic>
<author><persName><forename>Roberto</forename><surname>Amadio</surname></persName>
<affiliation>
<orgName type="laboratory">PPS</orgName>
<orgName type="team">Preuves, Programmes et Systèmes</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UMR7126</orgName>
<orgName type="institution">Université Paris VII - Paris Diderot</orgName>
</affiliation>
</author>
<author><persName><forename>Patrick</forename><surname>Baillot</surname></persName>
<affiliation>
<orgName type="laboratory">LIP</orgName>
<orgName type="team">Laboratoire de l'Informatique du Parallélisme</orgName>
<country>FR</country>
<orgName type="institution">Université de Lyon</orgName>
<orgName type="institution">CNRS : UMR5668</orgName>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">École Normale Supérieure - Lyon</orgName>
<orgName type="institution">Université Claude Bernard - Lyon I</orgName>
</affiliation>
</author>
<author><persName><forename>Antoine</forename><surname>Madet</surname></persName>
<affiliation>
<orgName type="laboratory">PPS</orgName>
<orgName type="team">Preuves, Programmes et Systèmes</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UMR7126</orgName>
<orgName type="institution">Université Paris VII - Paris Diderot</orgName>
</affiliation>
</author>
<title type="main" level="a">An affine-intuitionistic system of types and effects: confluence and termination</title></analytic><monogr><imprint/></monogr><idno type="HALid">http://hal.archives-ouvertes.fr/hal-00438101</idno><idno type="HALFile">http://hal.archives-ouvertes.fr/hal-00438101/PDF/affreg_nolncs.pdf</idno></biblStruct>
</listBibl>
</listBibl>