Alceste Scalas

I am a lecturer (assistant professor) in Computer Science at Aston University, Birmingham, UK.

I joined Aston University in March 2019. Before, I was a Research Associate at Imperial College London, and member of the Mobility Reading Group directed by Prof. Nobuko Yoshida.

I earned my PhD in Computer Science in 2015, at the University of Cagliari (Italy). Before that, I worked as software developer in industry, and as research software engineer in several projects at CRS4 (Center for Advanced Studies, Research and Development in Sardinia).

Research interests

I am interested in the theory and practice of concurrent and distributed systems: how to design and develop correct and reliable applications, by building upon rigorous mathematical foundations.

My main research topics are: formal methods, concurrency theory, distributed systems, programming languages, type systems. I am particularly keen on producing theoretically-grounded tools and libraries to aid software design, development, and verification.

News

New publications:

• the paper “Verifying Message-Passing Programs with Dependent Behavioural Types” and its companion artifact have been accepted at PLDI 2019 (joint work with Nobuko Yoshida and Elias Benussi)
• the paper “Less is More: Multiparty Session Types Revisited” and its companion artifact have been accepted at POPL 2019 (joint work with Nobuko Yoshida);
• the paper “Precise subtyping for synchronous multiparty sessions” has been accepted for publication on the Journal of Logical and Algebraic Methods in Programming (joint work with Silvia Ghilezan, Svetlana Jakšić, Jovanka Pantović, and Nobuko Yoshida)

Events

• ICE 2019 (PC co-chair - “ICEcreamer”)
• ACM SAC-MiDOS 2019 (PC member)
• ISEC 2019 (PC member)
• ICE 2018 (PC member)
• ECOOP 2018 (Artifact Evaluation Committee member)
• ACM SAC-SOAP 2018 (PC member)
• ECOOP 2017 (Artifact Evaluation Committee member)
• ICE 2017 (PC member)
• ACM SAC-SOAP 2017 (PC member)

Tools

• Effpi: an experimental toolkit for strongly-typed message-passing programs in Dotty (a.k.a. the future Scala 3 programming language), with verification capabilities based on type-level model checking. (Companion paper) (Source code on GitHub)
• mpstk: a toolkit for specifying multiparty protocols and verifying their behavioural properties (e.g., deadlock-freedom, liveness, termination...). (Companion paper) (Source code on GitHub)
• lchannels: A Scala library for describing protocols as types, and write network programs that enjoy compile-time protocol checks. (Companion paper) (Source code on GitHub)
• Scribble-Scala: A Scala backend for the Scribble protocol language and verification tool. The backend (based on lchannels above) generates Scala classes and APIs providing compile-time checks for programs implementing multiparty protocols. (Companion paper) (Source code on GitHub)
• The LTS WorkBench: A Scala library for defining arbitrary labelled transition systems and behavioural properties, and verify them. (Companion paper)
• Erlang FFI (obsolete): Erlang virtual machine extensions for foreign function calls. These extensions were released before Native Implemented Functions (NIFs) for Erlang (and contributed to the debate that led to their adoption). (Companion paper)

Research projects

• Past:
  • 2018-2019 (at Imperial College London): From Data Types to Session Types - A Basis for Concurrency and Distribution - EPRSC grant EP/K034413/1
  • 2015-2018 (at Imperial College London): Conversation-Based Governance for Distributed Systems by Multiparty Session Types - EPRSC grant EP/K011715/1
  • 2012-2016 (at Università di Cagliari and Imperial College London): Behavioural Types for Reliable Large-Scale Software Systems (BETTY) - EU COST Action IC1201 - WG1 (Foundations) and WG2 (Security).
  • 2012-2015 (at Università di Cagliari): Security Horizons - MIUR PRIN 2010-11.
  • 2012-2015 (at Università di Cagliari): TESLA - Autonomous Region of Sardinia grant L.R.7/2007-CRP2_120.
  • 2012-2015 (at Università di Cagliari): TRICS - Autonomous Region of Sardinia grant L.R.7/2007-CRP-17285.
  • 2006-2010 (at CRS4): MIUR FAR 630 project "Innovative models and methodologies for control, diagnostics and management of combined gas-steam thermoelectric power plants, under highly variable and perturbed working conditions". Tasks: design, development and formal analysis of a framework for parallel and distributed real-time numerical computing, aimed at industrial applications. Author of the Foreign Function Interface for Erlang proposal (EEP 7).

Publications

(Also on DBLP)

• Alceste Scalas, Nobuko Yoshida, Elias Benussi. Effpi: Verified Message-Passing Programs in Dotty (tool paper). Proc. ACM SIGPLAN Scala Symposium 2019.
• Alceste Scalas, Nobuko Yoshida, Elias Benussi. Verifying Message-Passing Programs with Dependent Behavioural Types. Proc. PLDI 2019.
• Silvia Ghilezan, Svetlana Jakšić, Jovanka Pantović, Alceste Scalas, and Nobuko Yoshida. Precise subtyping for synchronous multiparty sessions. Journal of Logical and Algebraic Methods in Programming, Vol. 109, April 2019.
• Alceste Scalas, Nobuko Yoshida. Less is More: Multiparty Session Types Revisited. Proc. POPL 2019.
• Alceste Scalas, Nobuko Yoshida. Multiparty Session Types, Beyond Duality. Journal of Logical and Algebraic Methods in Programming, 2018.
• Alceste Scalas, Ornela Dardha, Raymond Hu, Nobuko Yoshida. A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming (+ artifact). Proc. ECOOP 2017.
• Alceste Scalas, Nobuko Yoshida. Multiparty Session Types, Beyond Duality (Abstract). Proc. PLACES 2017.
• Tzu-chun Chen, Mariangiola Dezani-Ciancaglini, Alceste Scalas, Nobuko Yoshida. On the Preciseness of Subtyping in Session Types. Logical Methods in Computer Science, 2017.
• Massimo Bartoletti, Alceste Scalas, Emilio Tuosto, Roberto Zunino. Honesty By Typing. Logical Methods in Computer Science, 2016.
• A. Scalas, N. Yoshida. Lightweight Session Programming in Scala (+ artifact). Proc. ECOOP 2016. For the latest version of the artifact, visit: http://alcestes.github.io/lchannels
• M. Bartoletti, M. Murgia, A. Scalas. R. Zunino. Verifiable abstractions for contract-oriented systems. Journal of Logical and Algebraic Methods in Programming, 2015.
• A. Scalas, M. Bartoletti. The LTS WorkBench. Proc. ICE 2015, 4-5 June 2015, Granoble, France. For the implementation, see the LTS WorkBench page
• M. Bartoletti, J. Lange, A. Scalas, R. Zunino. Choreographies in the wild. Accepted for publication in Science of Computer Programming, 2014.
• M. Bartoletti, A. Scalas, R. Zunino. A semantic deconstruction of session types. Proc. CONCUR'14, 1-6 September 2014, Rome, Italy. (For an extended version with proofs, see the PhD thesis below)
• M. Bartoletti, M. Murgia, A. Scalas, R. Zunino. Modelling and verifying contract-oriented systems in Maude. WRLA'14, 5-6 April 2014, Grenoble, France. Extended version available on the TCS publications page.
• J. Lange, A. Scalas. Choreography synthesis as contract agreement. ICE 2013, 6 June 2013 , Florence, Italy. Extended version available on the TCS publications page.
• M. Bartoletti, A. Scalas, E. Tuosto, R. Zunino. Honesty by typing. FORTE/FMOODS'13, 3-6 June 2013, Florence, Italy. Extended technical report available on the TCS publications page.
• A. Scalas, G. Casu, P. Pili. High-performance technical computing with Erlang. ACM SIGPLAN Erlang Workshop (satellite event of ACM ICFP), 27 September 2008.

Peer-reviewed workshops (without formal proceedings)

• M. Bartoletti, A. Scalas, R. Zunino. Towards a theory of honesty. HotSpot'14, 5 April 2014, Grenoble, France.
• M. Bartoletti, A. Scalas, E. Tuosto, R. Zunino. Honesty by typing (preliminar version). BEAT'13, 22 January 2013, Rome, Italy.
• M. Bartoletti, A. Scalas, E. Tuosto, R. Zunino. What if contracts are violated? (short paper). FLACOS'12, 19 September 2012, Bertinoro, Italy.

Seminars and invited talks

• Effpi: concurrent programming with dependent behavioural types (joint work with E. Benussi and N. Yoshida). Presented at:
  • BEAT 2019 (13 January 2019). Middlesex University London (Theory of Computing and AI Seminars), 26th October 2018.
  • VeTSS school / FMATS workshop, Microsoft Research Cambridge, 25 September 2018.
  • University of Novi Sad (Serbia), 17 September 2018.
• Lightweight session programming in Scala (joint work with N. Yoshida). Presented at:
  • S-REPLS 6, University College London, 25 May 2017.
  • University of Novi Sad (Serbia), 27 March 2017.
  • University of Cagliari (Italy), 7 July 2016.
• Dagstuhl seminar: Theory and Applications of Behavioural Types. Schloss Dagstuhl, 29 Jan -- 3 Feb 2017.
• Multiparty session types and their applications. Univ. of Novi Sad (Serbia), 4 March 2016 (with N. Yoshida).
• A gentle introduction to concurrency theory. CRS4, May 26, 2015.
• A semantic deconstruction of session types (joint work with M. Bartoletti and R. Zunino). Presented at:
  • Imperial College London, December 4, 2014.
  • University of Glasgow, February 3, 2015.
• Contract-oriented computing in CO₂ (joint work with M. Bartoletti, E. Tuosto, and R. Zunino). Presented at:
  • University of Cagliari - MSc Seminar, course on "Foundations of security" (December 17-18, 2013)
  • OPLSS 2013 Student Talks (August 1, 2013)
  • University of Cagliari - PhD/MSc Seminar, course on "Foundations of security" (March 26, 2013)
  • University of Pisa - "Mauriana Pesaresi" PhD Seminars (December 13, 2012)
  • University of Leicester - PhD Seminars (October 4, 2012)
  • FOSAD 2012 - open session (September 8, 2012)

PhD Thesis

A semantic deconstruction of session types. Successfully defended on May 2015 (final score: excellent)

• PhD thesis reviewers: Simon Gay, Luca Padovani
• PhD commission: Rocco De Nicola (president), Marco Tarini, Nicoletta Dessì

Other writings

• M. Bartoletti, T. Cimoli, A. Scalas. Notes on contract-oriented computing (2013).
• A. Scalas. On the security of social networks - Literature review on ReBAC policies and Sybil defences (2012).