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

Roberto M. Amadio; Patrick Baillot; Antoine Madet

hal-00625760, version 1

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

Roberto M. Amadio () ¹, Patrick Baillot () ², Antoine Madet ( Author to contact preferably ) ¹

Workshop LOLA "Syntax and Semantics of Low Level Languages" (2010)

Abstract: 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-00625760, version 1
http://hal.archives-ouvertes.fr/hal-00625760
oai:hal.archives-ouvertes.fr:hal-00625760
From: Antoine Madet <>
Submitted on: Thursday, 22 September 2011 15:45:00
Updated on: Monday, 30 April 2012 12:04:55

See detailed view

Export

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>Congres communications</head>
<biblStruct type="article" xml:id="hal-00625760"><analytic>
<author><persName><forename>Roberto M.</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><meeting>Workshop LOLA "Syntax and Semantics of Low Level Languages"</meeting><imprint><pubPlace><settlement>Edimbourg</settlement><country>United Kingdom</country></pubPlace></imprint></monogr><idno type="HALid">http://hal.archives-ouvertes.fr/hal-00625760</idno></biblStruct>
</listBibl>
</listBibl>