Editorial Work
ACM SIGLOG News - Editor of the Feature on "Conference Reports" (2015-2022) [URL]
Special Issue: Logical Methods in Computer Science [URL]
Best papers from FORTE'19 (co-editor with N. Yoshida)
Special Issue: Information and Computation (Elsevier), Vol. 275 [DOI] [URL]
Best papers from EXPRESS/SOS'18 (co-editor with S. Tini)
Proceedings of FORTE 2019 - 39th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems (co-editor with N. Yoshida)
Springer LNCS Vol. 11535 [DOI]
Proceedings of EXPRESS/SOS 2019 - Combined 26th International Workshop on Expressiveness in Concurrency and 16th Workshop on Structural Operational Semantics (co-editor with J. Rot)
EPTCS Vol. 300 [DOI]
Proceedings of EXPRESS/SOS 2018 - Combined 25th International Workshop on Expressiveness in Concurrency and 15th Workshop on Structural Operational Semantics (co-editor with S. Tini)
EPTCS Vol. 276 [DOI]
Proceedings of DCM 2015 - Eleventh International Workshop on Developments in Computational Models (co-editor with C. Muñoz)
EPTCS Vol. 204 [DOI]
Special Issue: Mathematical Structures in Computer Science (MSCS) - Cambridge University Press, Vol. 29 [DOI]
Best papers from ICTAC'15 (co-editor with M. Leucker, C. Rueda, and F. Valencia)
Book Chapters
Runtime Verification for Decentralised and Distributed Systems (with A. Francalanza and C. Sanchez)
In Lectures on Runtime Verification Springer LNCS, Vol. 10457. [DOI]
Journals
Asynchronous Session-Based Concurrency: Deadlock-freedom in Cyclic Process Networks (with B. van den Heuvel)
Supersedes our ICE'21 and EXPRESS/SOS'22 papers.
Comparing Session Type Systems derived from Linear Logic (with B. van den Heuvel)
Logical and Algebraic Methods in Programming [DOI] [DRAFT@arxiv]
Supersedes our PLACES'20 paper.
Minimal Session Types for the pi-calculus (with A. Arslanagic and A. Palamariuc)
Supersedes our PPDP'21 paper.
Non-Deterministic Functions as Non-Deterministic Processes (Extended Version) (with J. Paulus and D. Nantes-Sobrinho)
Supersedes our FSCD'21 paper.
Bit-Vector Typestate Analysis (with A. Arslanagic and P. Subotic)
Special Issue: Best Papers from iFM'22
Supersedes our iFM'22 paper.
Session-Based Concurrency in Maude: Executable Semantics and Type Checking (with C. Ramírez and J.C. Jaramillo)
Special Issue: Selected Papers from WRLA'22
Supersedes our WRLA'22 paper.
A Decentralized Analysis of Multiparty Protocols (with B. van den Heuvel)
Session Coalgebras: A Coalgebraic View on Regular and Context-Free Session Types (with A. C. Keizer and H. Basold)
ACM TOPLAS [DOI] [DRAFT]
Special Issue: Best Papers from ESOP'21
Supersedes our ESOP'21 paper.
Causal Consistency for Reversible Multiparty Protocols (with C. Mezzina)
Logical Methods in Computer Science Vol 17, Issue 4. [DOI] [DRAFT@arxiv]
Supersedes our PPDP'17 paper.
Comparing Type Systems for Deadlock Freedom (with O. Dardha)
Logical and Algebraic Methods in Programming: 124 [DOI] [DRAFT@arxiv]
Supersedes our EXPRESS'15 paper.
On Primitives for Compensation Handling as Adaptable Processes (with J. Dedeić and J. Pantović)
Logical and Algebraic Methods in Programming: 121 [PDF] [DOI]
Supersedes our EXPRESS'15 and SAC'17 papers with improved encodings and stronger correctness properties.
Session-Based Concurrency, Declaratively (with M. Cano, H. Lopez, and C. Rueda)
Acta Informatica 59: 1-87 [PDF] [DOI]
Supersedes our PPDP'15 paper. See also Mauricio's PhD thesis.
On the Relative Expressiveness of Higher-Order Session Processes (with D. Kouzapas and N. Yoshida)
Supersedes our ESOP'16 paper.
Reversibility in Session-Based Concurrency: A Fresh Look (with C. Mezzina)
Logical and Algebraic Methods in Programming 90:2-30 (2017)
Supersedes our PLACES'16 and ICTCS'16 papers.
Characteristic Bisimulation for Higher-Order Session Processes (with D. Kouzapas and N. Yoshida)
Acta Informatica 54(3): 271-341 (2017)
Special Issue: Best Papers from CONCUR'15 [DOI]
Event-Based Run-time Adaptation in Communication-Centric Systems (with C. Di Giusto)
Formal Aspects of Computing 28(4): 531-566 (2016)
Supersedes our WS-FM'14 paper.
Self-Adaptation and Secure Information Flow in Multiparty Communications (with I. Castellani and M. Dezani-Ciancaglini)
Formal Aspects of Computing 28(4): 669-696 (2016)
Supersedes our BEAT'14 paper.
Dynamic Role Authorization in Multiparty Conversations (with S. Ghilezan, S. Jaksic, J. Pantovic, and H. T. Vieira)
Formal Aspects of Computing 28(4): 643-667 (2016)
Supersedes our BEAT'14 and PLACES'15 papers.
Combining Behavioural Types With Security Analysis (with M. Bartoletti, I. Castellani, P.-M. Deniélou, M. Dezani-Ciancaglini, S. Ghilezan, J. Pantovic, P. Thiemann, B. Toninho, and H. T. Vieira)
Logical and Algebraic Methods in Programming 84:763–780 (2015)
Extends the state of the art report of BETTY Cost Action's WG2 [HAL] [DOI]
Disciplined Structured Communications with Disciplined Runtime Adaptation (with C. Di Giusto)
Science of Computer Programming 97: 235–265 (2015) [DOI] [PDF draft]
Supersedes our SAC'13 paper.
Linear Logical Relations and Observational Equivalences for Session-Based Concurrency (with L. Caires, F. Pfenning, and B. Toninho)
Information and Computation 239:254-302 (2014) [DOI] [PDF]
Supersedes our ESOP'12 paper.
Note: The version posted here addresses inaccuracies in Sect. 5.3 (confluence) as in previous versions of the paper.
Adaptable Processes (with M. Bravetti, C. Di Giusto, and G. Zavattaro)
Logical Methods in Computer Science Vol. 8(4:13) 2012, pp. 1–7 [DOI]
Supersedes our FORTE/FMOODS'11 paper.
On the Expressiveness and Decidability of Higher-Order Process Calculi (with I. Lanese, D. Sangiorgi and A. Schmitt)
Information and Computation 209(2):198-226 (2011) [DOI]
Supersedes our LICS'08 paper.
Higher-Order Concurrency: Expressiveness and Decidability
Bulletin of the EATCS 101:92-124 (2010) [LINK]
This is a survey of the main results in my PhD Thesis
Peer-Reviewed Contributions
[International Conferences and Workshops. Full and Short Papers]
Around Classical and Intuitionistic Linear Processes (with D. Frumin and J.C. Jaramillo)
CONCUR'24 LIPIcs, Vol. 311. [DOI] [DRAFT@arxiv (with appendices)]
Typed Non-determinism in Concurrent Calculi: The Eager Way (with B. van den Heuvel, J. Paulus, and D. Nantes-Sobrinho)
MFPS'24 ENTICS, to appear. [DOI] [DRAFT@arxiv (with appendices)]
Typed Non-determinism in Functional and Concurrent Calculi (with B. van den Heuvel, J. Paulus, and D. Nantes-Sobrinho)
APLAS'23 Springer LNCS, 14405. [DOI] [DRAFT@arxiv (with appendices)]
Monitoring Blackbox Implementations of Multiparty Session Protocols (with B. van den Heuvel and R. Dobre)
RV'23 Springer LNCS, 14245. [DOI] [DRAFT@arxiv (with appendices)]
Termination in Concurrency, Revisited (with J. Paulus and D. Nantes-Sobrinho)
PPDP'23 ACM Press. [DOI] [DRAFT@arxiv (with appendices)]
A Bunch of Sessions: A Propositions-as-Sessions Interpretation of Bunched Implications in Channel-Based Concurrency (with D. Frumin, E. D'Osualdo, and B. van den Heuvel)
OOPSLA'22 PACM, Volume 6, Issue OOPSLA2. [DOI] [DRAFT@arxiv (with appendices)]
Asynchronous Functional Sessions: Cyclic and Concurrent (with B. van den Heuvel)
EXPRESS/SOS'22 EPCTS, 368. [DOI] [DRAFT@arxiv (with appendices)]
Types and Terms Translated: Unrestricted Resources in Encoding Functions as Processes (with J. Paulus and D. Nantes-Sobrinho)
TYPES'21 (Post-proceedings) LIPIcs, Vol. 239. [DOI] [DRAFT@arxiv (with appendices)]
Scalable Typestate Analysis for Low-Latency Environments (with A. Arslanagic and P. Subotic)
iFM'22 Springer LNCS, 13274. [DOI] [DRAFT@arxiv] Best Artifact Award
Executable Semantics and Type Checking for Session-Based Concurrency in Maude (with C. Ramírez)
Minimal Session Types for the pi-calculus (with A. Arslanagic and A. Palamariuc)
PPDP'21 ACM Press. [DOI] [DRAFT] [DRAFT@arxiv]
Deadlock Freedom for Asynchronous and Cyclic Process Networks (with B. van den Heuvel)
Non-Deterministic Functions as Non-Deterministic Processes (with J. Paulus and D. Nantes-Sobrinho)
FSCD'21 LIPIcs, Vol. 195. [DOI] [DRAFT@arxiv (with appendices)]
Session Coalgebras: A Coalgebraic View on Session Types and Communication Protocols (with A. C. Keizer and H. Basold)
ESOP'21 Springer LNCS, Vol. 12648. [DOI] [DRAFT@arxiv (with appendices)]
Hyperledger Fabric: Evaluating Endorsement Policy Strategies in Supply Chains (with M. Soelman, V. Andrikopoulos, V. Theodosiadis, K. Goense, and A. Rutjes)
Session Type Systems based on Linear Logic: Classical versus Intuitionistic (with B. van den Heuvel)
Domain-Aware Session Types (with L. Caires, F. Pfenning, and B. Toninho.)
CONCUR'19 LIPIcs, Vol. 140. [DOI] [DRAFT@arxiv (with appendices)]
Minimal Session Types (with A. Arslanagic and E. Voogd)
ECOOP'19 LIPIcs, Vol. 134. [DOI] [DRAFT@arxiv (with appendices)] [artifact] [video]
Reversible Choreographies in Haskell (with F. de Vries)
Relating Process Languages for Security and Communication Correctness (Extended Abstract) (with D. Nantes-Sobrinho)
FORTE'18 Springer LNCS, to appear. [DOI] [DRAFT (with appendices)]
Linearity, Control Effects, and Behavioural Types (with L. Caires)
ESOP'17 Springer LNCS, Vol. 10201. [DOI] [DRAFT] [DRAFT (with appendices)]
Causally Consistent Reversible Choreographies (with C. Mezzina)
PPDP'17 ACM Press. [DOI] [DRAFT] [DRAFT@arXiv (March 2017)]
Session-Based Concurrency, Reactively (with J. Arias and M. Cano)
FORTE'17 Springer LNCS, Vol. 10321. [DOI] [DRAFT] [DRAFT (with appendices)]
Supersedes a draft entitled "A Reactive Interpretation of Session-Based Concurrency'' [DRAFT], presented at ICTCS'16 (see below) - REBLS'16 (co-located with SPLASH'16) - BETTY Final Meeting (October 6-7, 2016)
Efficient Compensation Handling via Subjective Updates (with J. Dedeić and J. Pantović)
SAC'17 (CASM track) ACM Press. [DOI] [DRAFT]
Towards A Practical Model of Reactive Communication-Centric Software (with J. Arias and M. Cano)
Multiparty Session Types Within A Canonical Binary Theory, and Beyond (with L. Caires)
FORTE'16 Springer LNCS, Vol. 9688. [DOI] [DRAFT] [DRAFT (with proofs)]
The Challenge of Typed Expressiveness in Concurrency
On the Relative Expressiveness of Higher-Order Session Processes (with D. Kouzapas and N. Yoshida)
More details in the dedicated page.
Reversible Sessions Using Monitors (with C. Mezzina)
Comparing Deadlock-Free Session Typed Processes (with O. Dardha)
EXPRESS/SOS'15 EPCTS, Vol. 190. [DOI]. [DRAFT] (with proofs).
On Compensation Primitives as Adaptable Processes (with J. Dedeić and J. Pantović)
EXPRESS/SOS'15 EPCTS, Vol. 190. [DOI] [DRAFT] [DRAFT (with proofs)]
Characteristic Bisimulations for Higher-Order Session Processes (with D. Kouzapas and N. Yoshida)
CONCUR'15 LIPIcs, Vol. 42. [DOI] [DRAFT] More details in the dedicated page.
Declarative Interpretations of Session-Based Concurrency (with M. Cano, H. Lopez, and C. Rueda)
A Typed Model for Dynamic Authorizations (with S. Ghilezan, S. Jaksic, J. Pantovic, and H. T. Vieira)
Self-Adaptation and Secure Information Flow in Multiparty Structured Communications: A Unified Perspective (with M. Dezani-Ciancaglini, and I. Castellani)
Dynamic Role Authorization in Multiparty Conversations (with S. Ghilezan, S. Jaksic, J. Pantovic, and H. T. Vieira)
An Event-Based Approach to Runtime Adaptation in Communication-Centric Systems (with C. Di Giusto)
WS-FM'14 Springer LNCS, Vol. 9421. [DOI] [DRAFT (with proofs)] [HAL]
Towards Global and Local Types for Adaptation (with M. Bravetti, M. Carbone, I. Lanese, T. Hildebrandt, J. Mauro and G. Zavattaro.)
Towards Formal Interaction-based Models of Grid Computing Infrastructures (with C. Ramirez, J. Aranda, and J. F. Diaz.)
Behavioral Polymorphism and Parametricity in Session-Based Communication (with L. Caires, F. Pfenning, and B. Toninho.)
Session Types with Runtime Adaptation: Overview and Examples (with C. Di Giusto)
Disciplined Structured Communications with Consistent Runtime Adaptation (with C. Di Giusto)
SAC'13 (SOAP track) ACM Press. [DOI] [PDF] [PDF extended version] (01/03/2014)
Towards the Verification of Adaptable Processes (with M. Bravetti, C. Di Giusto, and G. Zavattaro)
Linear Logical Relations for Session-Based Concurrency (with L. Caires, F. Pfenning, and B. Toninho)
Adaptable Processes (Extended Abstract) (with M. Bravetti, C. Di Giusto, and G. Zavattaro)
FMOODS-FORTE'11. Springer LNCS, Vol. 6722. [DOI] [PDF] - see here for more details.
Type-Based Access Control for Data-Centric Systems (with L. Caires, J. Seco, H. T. Vieira, and L. Ferrão)
Steps on the Road to Component Evolvability (with M. Bravetti, C. Di Giusto, and G. Zavattaro)
Time and Exceptional Behavior in Multiparty Structured Interactions (with H. A. Lopez)
On the Expressiveness of Polyadic and Synchronous Communication in Higher-Order Process Calculi (with I. Lanese, D. Sangiorgi and A. Schmitt)
An Overview of FORCES: An INRIA Project on Declarative Formalisms for Emergent Systems (with J. Aranda, G. Assayag, C. Olarte, C. Rueda, M. Toro, and F. Valencia)
On the Expressiveness of Forwarding in Higher-Order Communication (with C. Di Giusto and G. Zavattaro)
Towards a Unified Framework for Declarative Structured Communications (with H. A. Lopez and C. Olarte)
On the Expressiveness and Decidability of Higher-Order Process Calculi (with I. Lanese, D. Sangiorgi and A. Schmitt)
Stochastic Behavior and Explicit Discrete Time in Concurrent Constraint Programming (with J. Aranda, C. Rueda and F. Valencia)
Non-determinism and Probabilities in Timed Concurrent Constraint Programming (with C. Rueda)
Timed Concurrent Constraint Programming for Analysing Biological Systems (with J. Gutiérrez, C. Rueda and F. Valencia)
A Declarative Framework for Security: Secure Concurrent Constraint Programming (Poster) (with H. López, C. Palamidessi, C. Rueda and F. Valencia).
Implementing an Abstraction Scheme for Soft Constraints (with A. Delgado and C. Rueda)
Implementing Semiring-Based Constraints using Mozart (with A. Delgado, C. Olarte and C. Rueda)
An Interactive Tool for the Controlled Execution of an Automated Timetabling Constraint Engine (with A. Delgado, G. Pabon, R. Jordan, C. Rueda and J.F. Diaz.)
Drafts and Submissions
A Typeful Characterization of Multiparty Structured Conversations Based on Binary Sessions (with L. Caires) [DRAFT] [DRAFT@arXiv]
Some public presentations related to this work:
OPCT'14 (18/06/14) with the title "Bridging the Gap between Binary and Multiparty Communications" [SLIDES]
BETTY meeting (13/04/2014) with the title "Relating Multiparty and Binary Session Types via Linear Logic"
Logical Foundations for Domain-Aware Concurrency (with L. Caires, F. Pfenning, and B. Toninho) [DRAFT]
Presented at MSC'14 (12/02/2014) and at Comete-Parsifal seminar - LIX, Ecole Polytechnique (7/11/2013)
Superseded by our CONCUR'19 paper (see below)
Technical Reports
Multiparty Reactive Sessions (with M. Cano, I. Castellani, and C. Di Giusto)
Core Higher-Order Session Processes: Tractable Equivalences and Relative Expressiveness (with D. Kouzapas and N. Yoshida)
This TR comprises papers first published in CONCUR'15 and ESOP'16 and later in Acta Informatica (2017) and Information and Computation (2019), respectively. More details in the dedicated page.
Relational Parametricity for Polymorphic Session Types (with L. Caires, F. Pfenning, and B. Toninho.)
Technical Report CMU-CS-12-108, April 2012. Click here for a draft.
Higher-Order Concurrency: Expressiveness and Decidability Results (PhD Thesis)
Technical Report UBLCS-2010-07, May 2010. [PDF]
Theses
Higher-Order Concurrency: Expressiveness and Decidability Results [PDF]
Dottorato di Ricerca in Informatica, University of Bologna, 2010.
Supervisor: Davide Sangiorgi
External Reviewers: Uwe Nestmann (Berlin) and Nobuko Yoshida (London)
Examination Committee: Mariangiola Dezani (Turin), Paola Quaglia (Trento), Francesco Romani (Pisa).
Soft Constraints in Concurrent Constraint Programming: Design and Implementation (with Alberto Delgado) (Análisis e Implementación de Mecanismos de Restricciones Débiles para Programación Concurrente por Restricciones)
Engineering Degree in Computer Science, Universidad Javeriana (Colombia), February 2006.
Work awarded for the achievements accomplished, Council of the School of Engineering, February 10, 2006
Other Works
Towards a Behavioral Type System for Reconfigurable Systems (with K. Suenaga)
The 22nd Nordic Workshop on Programming Theory - NWPT '10, 10-12 November 2010, Turku, Finland
Move vs Copy: Towards a Formal Comparison of Ambients and Higher-Order Process Calculi (with C. Di Giusto)
The 11th Italian Conference on Theoretical Computer Science - ICTCS'09, 28-29 September 2009, Cremona, Italy
Languages for Concurrency Featuring Quantitative Information: An Overview and New Perspectives (with J. Aranda)
Newsletter of the ALP, Vol 22 n.1. March 2009. DOWNLOAD draft as PDF
Process Calculi to Analyze Emerging Applications in Concurrency (with A. Arbeláez, A Aristizabal, J. Gutiérrez, H. A. Lopez, C. Rueda and F. Valencia)
Unpublished manuscript. DOWNLOAD draft as PDF.
Timed Concurrent Constraint Programming in Systems Biology (with A. Arbeláez and J. Gutiérrez).
Newsletter of the ALP, Vol. 19 n. 4, November/December 2006. DOWNLOAD draft as PDF.
Modelling Biological Systems using Process Calculi (In Spanish, with J. Gutierrez and C. Rueda.)
Epiciclos Journal, Vol. 4 (1), 79-101. (2005). ISSN: 1657-5636. DOWNLOAD draft as PDF
Semiring-based Fuzzy Constraints in Concurrent Constraint Programming (with A. Delgado, C. Olarte and C. Rueda.)
XXXI Latin American Computing Conference (CLEI 2005). ISBN: 958-670-426-2. ©CLEI, 2005. PDF
Implementing Semiring-Based Constraints using a Concurrent Constraint Programming Language (with A. Delgado, C. Olarte and C. Rueda).
Sixth International Workshop on Preferences and Soft Constraints. Part of CP 2004. September 2004. PDF