Author name cluster

António Ravara

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

2 papers

1 author row

I&C Journal 2012 Journal Article

An Algebra of Behavioural Types

António Ravara
Pedro Resende
Vasco T. Vasconcelos

We propose a process algebra, the Algebra of Behavioural Types, as a language for typing concurrent objects. A type is a higher-order labelled transition system that characterises all possible life cycles of a concurrent object. States represent interfaces of objects; state transitions model the dynamic change of object interfaces. Moreover, a type provides an internal view of the objects that inhabits it: a synchronous one, since transitions correspond to message reception. To capture this internal view of objects we define a notion of bisimulation, strong on labels and weak on silent actions. We study several algebraic laws that characterise this equivalence, and obtain completeness results for image-finite types.

Details DOI

TCS Journal 2006 Journal Article

Type checking a multithreaded functional language with session types

Vasco T. Vasconcelos
Simon J. Gay
António Ravara

We define a language whose type system, incorporating session types, allows complex protocols to be specified by types and verified by static type checking. A session type, associated with a communication channel, specifies the state transitions of a protocol and also the data types of messages associated with transitions; thus type checking can verify both correctness of individual messages and correctness of sequences of transitions. Previously, session types have mainly been studied in the context of the π -calculus; instead, our formulation is based on a multithreaded functional language with side-effecting input/output operations. Our typing judgements statically describe dynamic changes in the types of channels, and our function types not only specify argument and result types but also describe changes in channels. We formalize the syntax, semantics and type checking system of our language, and prove subject reduction and runtime type safety theorems.

Details DOI