1. Minimal Session Types for the pi-calculus (with A. Arslanagic and A. Palamariuc)

   • Information and Computation [DOI] [DRAFT@arxiv]

   • Supersedes our PPDP'21 paper.

2. Non-Deterministic Functions as Non-Deterministic Processes (Extended Version)  (with J. Paulus and D. Nantes-Sobrinho)

   • Logical Methods in Computer Science [DOI] [DRAFT@arxiv]

   • Supersedes our FSCD'21 paper.

3. Bit-Vector Typestate Analysis (with A. Arslanagic and P. Subotic)

   • Formal Aspects of Computing [DOI]

   • Special Issue: Best Papers from iFM'22

   • Supersedes our iFM'22 paper.

4. Session-Based Concurrency in Maude: Executable Semantics and Type Checking  (with C. Ramírez and J.C. Jaramillo) 

   • Logical and Algebraic Methods in Programming [DOI]

   • Special Issue: Selected Papers from WRLA'22

   • Supersedes our WRLA'22 paper.

5. A Decentralized Analysis of Multiparty Protocols (with B. van den Heuvel)

   • Science of Computer Programming [DOI] [PDF] [DRAFT@arxiv]

6. 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.

7. 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.

8. Comparing Type Systems for Deadlock Freedom (with O. Dardha) 

   • Logical and Algebraic Methods in Programming: 124 [DOI] [DRAFT@arxiv]

   • Supersedes our EXPRESS'15 paper.

9. 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.

10. 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. 

11. On the Relative Expressiveness of Higher-Order Session Processes (with D. Kouzapas and N. Yoshida)

    • Information and Computation 268 [DRAFT] [DOI]

    • Supersedes our ESOP'16 paper.

12. Reversibility in Session-Based Concurrency: A Fresh Look (with C. Mezzina) 

    • Logical and Algebraic Methods in Programming 90:2-30 (2017) 

    • Special issue: Best papers from PLACES'16. [DRAFT] [DOI]

    • Supersedes our PLACES'16 and ICTCS'16 papers.

13. 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] 

14. Event-Based Run-time Adaptation in Communication-Centric Systems (with  C. Di Giusto)  

    • Formal Aspects of Computing 28(4): 531-566 (2016) 

    • Special Issue on Behavioral Types [DOI] (Open access) [PDF] 

    • Supersedes our WS-FM'14 paper.

15. 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)

    • Special Issue on Behavioral Types [DOI] (Open access) [PDF]   

    • Supersedes our BEAT'14 paper.

16. 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)

    • Special Issue on Behavioral Types [DOI] [PDF]  

    • Supersedes our BEAT'14 and PLACES'15 papers.

17. 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] 

18. 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.

19. 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.

20. 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.

21. 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.

22. 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

[International Conferences and Workshops. Full and Short Papers]

• 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)

  • WRLA'22 Springer LNCS, 13252.  [DOI] [DRAFT]

• 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)

  • ICE'21  EPCTS, Vol. 347. [DOI] [DRAFT]

• 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)

  • DAPPS'20 IEEE [DOI]

• Session Type Systems based on Linear Logic: Classical versus Intuitionistic (with B. van den Heuvel)

  • PLACES'20  EPCTS, Vol. 314. [DOI] [DRAFT] [video]

• 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)

  • TFP'18 Springer LNCS, Vol. 11457. [DOI] [DRAFT]

• 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) 

  • ICTCS'16  Short communication - CEUR Workshop Proceedings, Vol 1720, 227 - 233 [URL] [DRAFT]   

• 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 

  • FORTE'16  Springer LNCS, Vol. 9688. [DOI] [DRAFT] 

  • This is a short position paper; comments are most welcome.

• On the Relative Expressiveness of Higher-Order Session Processes (with D. Kouzapas and N. Yoshida)

  • ESOP'16  Springer LNCS, Vol. 9632. [DOI] [DRAFT] 

  • More details in the dedicated page. 

• Reversible Sessions Using Monitors (with C. Mezzina)

  • PLACES'16  EPCTS, Vol. 211. [DOI] [DRAFT] 

• 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)

  • PPDP'15  ACM Press. [DOI] [DRAFT]

• A Typed Model for Dynamic Authorizations (with S. Ghilezan, S. Jaksic, J. Pantovic, and H. T. Vieira) 

  • PLACES'15  EPCTS, Vol 203. [DOI] [DRAFT] 

• Self-Adaptation and Secure Information Flow in Multiparty Structured Communications: A Unified Perspective (with M. Dezani-Ciancaglini, and I. Castellani) 

  • BEAT'14  EPCTS, Vol. 162. [DOI] [DRAFT] 

• Dynamic Role Authorization in Multiparty Conversations (with S. Ghilezan, S. Jaksic, J. Pantovic, and H. T. Vieira) 

  • BEAT'14  EPCTS, Vol. 162. [DOI] [DRAFT] 

• 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.) 

  • BEAT 2. Springer LNCS, Vol. 8368. [DOI] [PDF] 

• Towards Formal Interaction-based Models of Grid Computing Infrastructures (with C. Ramirez, J. Aranda, and J. F. Diaz.) 

  • DCM'13. EPTCS, Vol. 144. [DOI] [PDF] 

  • The full model overviewed in this paper can be found here.

• Behavioral Polymorphism and Parametricity in Session-Based Communication (with L. Caires, F. Pfenning, and B. Toninho.)

  • ESOP'13. Springer LNCS, Vol. 7792. [DOI] [PDF] [Slides] 

• Session Types with Runtime Adaptation: Overview and Examples (with C. Di Giusto) 

  • PLACES'13 (Slides). EPTCS, Vol. 137. [DOI] [PDF] This the post-proceedings version.

• 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)

  • ISoLA'12. Springer LNCS, Vol. 7609. [DOI] [PDF]

• Linear Logical Relations for Session-Based Concurrency (with L. Caires, F. Pfenning, and B. Toninho)

  • ESOP'12 Springer LNCS, Vol. 7211. [DOI] [PDF] (Extended version superseded by I&C journal version.) Slides  

  • [This paper supersedes a draft entitled "Termination in Session-Based Concurrency via Linear Logical Relations"]

• 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)

  • ESOP'11. Springer LNCS, Vol. 6602. [DOI] [PDF].

• Steps on the Road to Component Evolvability (with M. Bravetti, C. Di Giusto, and G. Zavattaro)

  • FACS'10. Springer LNCS, Vol. 6921. [DOI] [PDF] 

• Time and Exceptional Behavior in Multiparty Structured Interactions (with H. A. Lopez)

  • WS-FM'11. Springer LNCS, Vol. 7176. [DOI] [PDF]

• On the Expressiveness of Polyadic and Synchronous Communication in Higher-Order Process Calculi (with I. Lanese, D. Sangiorgi and A. Schmitt)

  • ICALP'10. Springer LNCS, Vol. 6199. [DOI] [PDF]

• 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)

  • ICLP'09. Springer LNCS, Vol. 5649. [DOI] [PDF]

• On the Expressiveness of Forwarding in Higher-Order Communication (with C. Di Giusto and G. Zavattaro) 

  • ICTAC'09. Springer LNCS, Vol. 5684. [DOI] [PDF]. A long version with proofs (34pp): [PDF]. Slides: [PDF]. More info see HERE

• Towards a Unified Framework for Declarative Structured Communications (with H. A. Lopez and C. Olarte)

  • PLACES'09. EPTCS, Vol 17, pp. 1-16. [DOI] [PDF]

• On the Expressiveness and Decidability of Higher-Order Process Calculi (with I. Lanese, D. Sangiorgi and A. Schmitt)

  • LICS'08. IEEE Computer Society, 2008. [DOI]  More information (abstract, long version with proofs) HERE

• Stochastic Behavior and Explicit Discrete Time in Concurrent Constraint Programming (with J. Aranda, C. Rueda and F. Valencia)

  • ICLP'08. Springer LNCS, Vol. 5366. [DOI] [PDF]

• Non-determinism and Probabilities in Timed Concurrent Constraint Programming (with C. Rueda)

  • ICLP'08. Springer LNCS, Vol. 5366. [DOI] [PDF]. An extended version (20pp), with examples: [PDF]

• Timed Concurrent Constraint Programming for Analysing Biological Systems (with J. Gutiérrez, C. Rueda and F. Valencia)

  • MeCBIC'06. Electronic Notes in Theoretical Computer Science (ENTCS), Vol 171/2 pp 117-137. Elsevier, 2007. [DOI] [PDF]

• A Declarative Framework for Security: Secure Concurrent Constraint Programming (Poster) (with H. López, C. Palamidessi, C. Rueda and F. Valencia).

  • ICLP'06. Springer LNCS, Vol. 4079. [DOI] [PDF]

• Implementing an Abstraction Scheme for Soft Constraints (with A. Delgado and C. Rueda)

  • SARA 2005. Springer LNCS, Vol. 3607. [DOI] [PDF]

• Implementing Semiring-Based Constraints using Mozart (with A. Delgado, C. Olarte and C. Rueda)

  • MOZ 2004. Springer LNCS, Vol. 3389. [DOI] [PDF]

• 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. Di­az.)

  • MOZ 2004. Springer LNCS, Vol. 3389. [DOI] [PDF]