Marco Giunti University of Oxford CV
Email: marco.giunti{change}gmail.com

Past groups: 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: coq, consensus, behavioural types, deadlock analysis, Go, pi calculus, oolong, distributed concurrency control, security, ocaml, why3

Upcoming events

• SAC 2025 (Programming Languages Track)
• ICFP 2024 (AEC)

Papers

• Behavioural up/down casting for statically typed languages. ECOOP 2024. With Lorenzo Bacchiani, Mario Bravetti, João Mota, António Ravara.
• 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

• SAC 2024 (Programming Languages Track)
• Coordination 2023