Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

Types for Deadlock-Free Higher-Order Concurrent Programs

Luca Padovani 1, * Luca Novara 1
Abstract : Deadlock freedom is for concurrent programs what progress is for sequential ones: it indicates the absence of stable (i.e., irreducible) states in which some pending operations cannot be completed. In the particular case of communicating processes, operations are inputs and outputs on channels and deadlocks may be caused by mutual dependencies between communications. In this work we define an effect system ensuring deadlock freedom of higher-order programs that communicate over linear channels and study its integration with polymorphic and recursive types.
Document type :
Preprints, Working Papers, ...
Complete list of metadata

Cited literature [35 references]  Display  Hide  Download

https://hal.inria.fr/hal-00954364
Contributor : Luca Padovani <>
Submitted on : Saturday, March 1, 2014 - 7:00:57 PM
Last modification on : Monday, March 3, 2014 - 1:35:14 PM
Long-term archiving on: : Friday, May 30, 2014 - 3:51:55 PM

File

PadovaniNovara14.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00954364, version 1

Citation

Luca Padovani, Luca Novara. Types for Deadlock-Free Higher-Order Concurrent Programs. 2014. ⟨hal-00954364⟩

Share

Metrics

Record views

381

Files downloads

191