Publications

1. Session Coalgebras: A Coalgebraic View on Regular and Context-Free Session Types (with A. C. Keizer and H. Basold)

   • ACM TOPLAS (In Press) [DOI] [DRAFT]

   • Special Issue: Best Papers from ESOP'21

   • Supersedes our ESOP'21 paper.

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

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

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

   • Supersedes our EXPRESS'15 paper.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

• Scalable Typestate Analysis for Low-Latency Environments (with A. Arslanagic and P. Subotic)

  • iFM'22 Springer LNCS, to appear. [DOI] [DRAFT@arxiv]

• Executable Semantics and Type Checking for Session-Based Concurrency in Maude (with C. Ramírez)

  • WRLA'22 Springer LNCS, to appear. [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]