Marco Giunti
University of Algarve
CV
Email: mgiunti 
ualg.pt
Past groups:
MRG, UOxford;
NOVA LINCS, UNOVA;
LASIGE,
ULisboa;
RELEASE,
UBI;
COMETE, Ecole Polytechnique
My main interest is to study language-based techniques for the analysis and deployment
of correct distributed mobile systems
Keywords:
multiparty session types,
typestates,
pi calculus,
coq,
why3,
ocaml,
go,
java
Upcoming events
Papers
- Type Congruence, Duality, and Iso-Recursive Session Types.
Gul Agha Festschrift 2025.
With Nobuko Yoshida.
LNCS 16120
- Iso-Recursive Multiparty Sessions and their Automated Verification.
ESOP 2025.
With Nobuko Yoshida.
Arxiv version
Talk @NOVA LINCS
Talk @ESOP
- Behavioural up/down casting for statically typed languages.
ECOOP 2024.
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
-
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.
-
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
- 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
- Secure implementations of typed channel abstractions. POPL 2007
(Talk, FCUL).
With Michele Bugliesi.
Full version 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
Communications and Reports
- Type Congruence, Duality, and Iso-Recursive Session Types.
PLACES 2025.
With Nobuko Yoshida.
Talk proposal
Slides
- Behavioural up/down casting for statically typed languages.
30 Years of Session Types.
With Lorenzo Bacchiani, Mario Bravetti, João Mota, António Ravara.
-
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.
-
Compiling linear and static channels in Go. INForum 2019
(Talk) .
Draft available
-
Rewinding functions through CPS. An experience
report.
Report 2019, FACTOR Project
- A mechanized proof of correctness of the Horn algorithm.
Report 2019, FACTOR Project
- 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
(Paper,
Talk).
With Vasco T. Vasconcelos, Kohei Honda and Nobuko Yoshida
- Preventing intrusions through non-interference. MCIS 2006.
Paper
available
Mechanisations
-
Iso-Recursive Binary Session Types.
Github 2025.
-
Iso-Recursive Multiparty Sessions and their Automated Verification.
Zenodo 2025
.
With Nobuko Yoshida.
-
A Mechanisation for a Typed Semantics of the Linear Pi Calculus.
Zenodo 2024
.
With Adrian Francalanza, António Ravara.
-
AtomiS: data-centric concurrency control made simple.
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
Running projects
Recently completed projects
- Smart Types and Smart Virtual Machines for Validated Smart Contracts (Co-Pi).
FCT, Portugal
- POST: Protocols, Observabilities and Session Types. EPSRC, UK
- Trustworthy and Resilient Decentralised Intelligence for Edge Systems
(TaRDIS)
-
Quantified Information Flow Control in Cloud Computing Systems.
DSTL, UK
- Behavioural Application Program Interfaces
(BEHAPI)
- 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
Last update: September 2025