Papers

• Behavioural up/down casting for statically typed languages. 30 Years of Session Types. With Lorenzo Bacchiani, Mario Bravetti, João Mota, António Ravara.
• AtomiS: Data-centric synchronization made practical. OOPSLA 2023. With Hervé Paulino, Ana Matos, António Ravara, Jan Cederquist, João Matos. Arxiv version
• On using VeriFast, VerCors, Plural, and KeY to check object usage. ECOOP 2023 (Talk). With João Mota and António Ravara. Arxiv version
• Type qualifier inference and code synthesis for a better data-centric synchronisation experience. ICE 2023. With Ana Matos, António Ravara, Hervé Paulino, Jan Cederquist, João Matos.
• Anticipation of Method Execution in Mixed Consistency Systems. SAC 2023 (Talk). With Hervé Paulino and António Ravara. Arxiv version
• A Java typestate checker supporting inheritance. SCP 2022 (ScienceDirect). With Lorenzo Bacchiani, Mario Bravetti, João Mota and António Ravara.
• Java Typestate Checker. Coordination 2021. SpringerLink With João Mota and Antonio Ravara.
• GoPi: Compiling linear and static channels in Go. Coordination 2020 (Talk). SpringerLink . See the demo in the webpage of the tool.
• Rewinding functions through CPS. An experience report. Report 2019, FACTOR Project
• A mechanized proof of correctness of the Horn algorithm. Report 2019, FACTOR Project
• Compiling linear and static channels in Go. INForum 2019 (Talk) . Draft available
• Linearity, session types and the pi calculus. MSCS 26(2) 2016. With Vasco T. Vasconcelos, preprint available
• Unlocking blocked communicating processes. WWV 2015. With Adrian Francalanza and Antonio Ravara.
• Static semantics of secret channel abstractions. NordSec 2014 (Talk) . Draft available
• Towards static deadlock resolution in the pi calculus. TGC 2013. With Antonio Ravara. LNCS preprint available
• Algorithmic type checking for a pi-calculus with name matching and session types. JLAP 82(8) 2013 . Draft available
• Hide and new in the pi-calculus. EXPRESS 2012. With Catuscia Palamidessi and Frank D. Valencia
• Typed observational equivalence for sessions. Report 2011
• A type checking algorithm for qualified session types. WWV 2011 (Talk). Also available as INRIA report. A tutorial in Behavioural Types Workshop
• A linear account of session types in the pi calculus. CONCUR 2010 (Talk). With Vasco T. Vasconcelos. Full version available
• Type safety without subject reduction for session types. Draft 2010 (Talk, IMT). With Vasco T. Vasconcelos, Kohei Honda and Nobuko Yoshida
• Session based type-discipline for pi calculus with matching. PLACES 2009 (Talk). With Vasco T. Vasconcelos, Kohei Honda and Nobuko Yoshida
• Secure implementations of typed channel abstractions. POPL 2007 (Talk, FCUL). With Michele Bugliesi. Full version available
• Preventing intrusions through non-interference. MCIS 2006. Paper available
• Typed processes in untyped contexts. TGC 2005. With Michele Bugliesi
• Security properties for intrusion detection. NordSec 2004
• PhD Dissertation. University of Venice TD-2007-1

Mechanisations

• AtomiS-Coq proof of type preservation. Zenodo 2022. With Ana Matos, António Ravara, Hervé Paulino, Jan Cederquist, João Matos. Instructions

Source Code

• The GoPi compiler. OCaml, builds on NordSec 2014
• LOCKRES: a session type checker resolving deadlocks. SML/NJ, builds on TGC 2013 and WWV 2011

Past events

• Coordination 2023

Running projects

• Quantified Information Flow Control in Cloud Computing Systems (Dstl)
• European Research Network on Formal Proofs (EUROPROOFNET)
• Behavioural Application Program Interfaces (BEHAPI)

Recently completed projects

• European research network on types for programming and verification (EUTYPES)
• Distributed Data-Centric Concurrency Control (DEDUCE)
• Functional Approach Teaching Portuguese Courses (FACTOR) Kickoff : 1 2
• Behavioural Types for Reliable Large-Scale Software Systems (BETTY)

Links

• Five stages of accepting constructive mathematics
• Europe needs strong software research
• Have fun with golang interfaces!
• Yes we LEGO
• Type Theory (Stanford Encyclopedia of Philosophy)
• Pi calculus tutorial. Robin Milner (1991), LFCS Edinburgh
• Barbie can be a good programmer! Read the story about girls that cannot be coders