Alceste Scalas

DTU Compute — Technical University of Denmark
DK-2800 Kongens Lyngby, Denmark
alcsc (at) dtu (dot) dk

I am an Associate Professor at DTU Compute — the Department of Applied Mathematics and Computer Science of the Technical University of Denmark. I am a member of the Software Systems Engineering research section.

I joined DTU in September 2020. Earlier, I was a Lecturer (Assistant Professor) in Computer Science at Aston University, Birmingham, UK. Before that, I was a Research Associate at Imperial College London (Dept. of Computing), 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

• March 2023: We are hiring! We are looking for a postdoctoral researcher (2 years) with experience in formal methods for distributed systems and/or programming language. The positions are part of the Horizon Europe project TaRDIS. For more details, please see this announcement (application deadline: 21 May 2023, Danish time). Feel free to contact me for inquiries.
• October 2022: the paper “Precise Subtyping for Asynchronous Multiparty Sessions” (extended journal version) has been accepted for publication on ACM Transactions on Computational Logic (joint work with Silvia Ghilezan, Jovanka Pantović, Ivan Prokić, and Nobuko Yoshida).
• June 2022: the paper “Generalised Multiparty Session Types with Crash-Stop Failures” has been accepted at CONCUR 2022 (joint work with Adam D. Barwell, Nobuko Yoshida, and Fangyi Zhou).
• May 2022: my project Hyben - Hybrid Verification of Heterogeneous Message-Passing Applications has been granted funding by the Danmarks Frie Forskningsfond! Topic: studying how to best combine static and run-time verification (monitoring), to assess the correctness of distributed applications. If you would like to start a PhD on this topic, feel free to contact me.
• The paper “Precise subtyping for asynchronous multiparty sessions” has been accepted at POPL 2021 (joint work with Silvia Ghilezan, Jovanka Pantović, Ivan Prokić, and Nobuko Yoshida).
• I have been invited to talk about Effpi at Scala World 2019! The video is now available on YouTube.
• 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 J.akšić, Jovanka Pantović, and Nobuko Yoshida)

Current research projects

• 2023-2026: TaRDIS - Trustworthy and Resilient Decentralised Intelligence for edge Systems (funded by the Horizon Europe programme)
• 2022-2026: Hyben - Hybrid Verification of Heterogeneous Message-Passing Applications (funded by the Danmarks Frie Forskningsfond)
• 2022-2025: Verification of Software-Defined Network configurations (Nordic Five Tech project in collaboration with the Theoretical Computer Science division at KTH, funded by DTU)
• 2021-2024: User-Friendly Formal Methods (PhD project co-supervisor, funded by DTU Compute)

Events

• PLACES 2023 (PC co-chair)
• VORTEX 2023 (PC member)
• COORDINATION 2023 (Artifact Evaluation Committee Chair)
• ICE 2023 (Steering Committee member)
• ICE 2022 (PC co-chair - “ICEcreamer”)
• COORDINATION 2022 (Artifact Evaluation Committee member)
• AMP 2022 (PC member)
• Dagstuhl Seminar: Behavioural Types: Bridging Theory and Practice (Co-organiser)
• TACAS 2021 (Artifact Evaluation Committee member)
• VORTEX 2021 (PC member)
• AMP 2021 (PC member)
• NWPT 2021 (PC member)
• ICE 2021 (PC co-chair - “ICEcreamer”)
• ICE 2020 (PC co-chair - “ICEcreamer”)
• AMP 2020 (PC member)
• 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)

Past Research projects

• 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

(A more complete and updated list is available 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).