Search

• < Previous
• 1
• Next >

---

Type Reconstruction for the Linear \pi-Calculus with Composite Regular Types

Luca Padovani.

We extend the linear {\pi}-calculus with composite regular types in such a way that data containing linear values can be shared among several processes, if there is no overlapping access to such values. We describe a type reconstruction algorithm for the extended type system and discuss some&nbsp;[&hellip;]

---

On Global Types and Multi-Party Session

Giuseppe Castagna ; Mariangiola Dezani-Ciancaglini ; Luca Padovani.

Global types are formal specifications that describe communication protocols in terms of their global interactions. We present a new, streamlined language of global types equipped with a trace-based semantics and whose features and restrictions are semantically justified. The multi-party sessions&nbsp;[&hellip;]

---

Typing Copyless Message Passing

Viviana Bono ; Luca Padovani.

We present a calculus that models a form of process interaction based on copyless message passing, in the style of Singularity OS. The calculus is equipped with a type system ensuring that well-typed processes are free from memory faults, memory leaks, and communication errors. The type system is&nbsp;[&hellip;]

---

On Sessions and Infinite Data

Paula Severi ; Luca Padovani ; Emilio Tuosto ; Mariangiola Dezani-Ciancaglini.

We define a novel calculus that combines a call-by-name functional core with session-based communication primitives. We develop a typing discipline that guarantees both normalisation of expressions and progress of processes and that uncovers an unexpected interplay between evaluation and&nbsp;[&hellip;]

---

Inference Systems with Corules for Combined Safety and Liveness Properties of Binary Session Types

Luca Ciccone ; Luca Padovani.

Many properties of communication protocols combine safety and liveness aspects. Characterizing such combined properties by means of a single inference system is difficult because of the fundamentally different techniques (coinduction and induction, respectively) usually involved in defining and&nbsp;[&hellip;]

---