Speakers / Predavači
Nobuko Yoshida and Alceste Scalas
Imperial College, UK
http://mrg.doc.ic.ac.uk/ (home page)
Title / Naslov:
Effpi: concurrent programming with dependent behavioural types
Abstract / Sažetak:
Concurrent and distributed programming is notoriously hard. Many languages and software toolkits address the challenge by offering high-level abstractions, such as message-passing processes and actors; they allow for intuitive reasoning, but do not formally ensure that a program implements a given specification.
I will talk about Effpi, a toolkit for strongly-typed concurrent programming in Dotty (a.k.a. Scala 3). Effpi allows to specify the intended behaviour of a message-passing application using types: i.e., if a program type-checks and compiles, then it will run and communicate as prescribed by its types.
The foundation of Effpi is a concurrent functional language with a novel blend of behavioural types (from the π-calculus theory), and a form of dependent types, extending to higher-order interaction (i.e., sending/receiving program thunks). This design has three main advantages. First, it allows to verify programs through a combination of type checking and model checking techniques. Second, it is directly implemented (via deep embedding) in Dotty, including a simplified API for strongly-typed actor-based programming. And third, its functional nature allows for an efficient runtime system, supporting highly concurrent programs with millions of interacting processes/actors.
date/vreme: September 17, 2018, 16:00
venue/mesto: Sala za sastanke na 3. spratu u KULI FTN