Subsistema
Docentes Universitário
Regime
Exclusividade
Vínculo
CT em Funções Públicas por tempo indeterminado
Marco Giunti is an Assistant Professor at University of Algarve. He works in the area of programming languages and formal verification. He has been Research Associate and Lecturer in top-level Research Centers and Universities, including: University of Oxford (UK), NOVA School of Science and Technology (Portugal), University of Lisbon (Portugal), Ecole Polytechnique (France). He recently published results on multiparty session types (ESOP'25) and object-oriented languages (ECOOP'24, OOPSLA'23, ECOOP'23, SAC'23). He co-chairs the programming languages track of the ACM Symposium on Applied Computing (SAC'26, SAC'25, SAC'24). He recently concluded the project "Smart types and smart virtual machines for validated smart contracts" (Co-PI) funded by Foundation for Science and Technology (Portugal).
Atividades
Atividades
Revisão ad hoc de artigos em revista. ACM SIGLOG NEWS - Editor of Conference Reports Column. ACM.
2025 - Presente. Organização de evento. 41st ACM/SIGAPP Symposium On Applied Computing - Co-chair of Programming Languages Track. Thessaloniki, Greece
March 23-27, 2026 (2025).
March 23-27, 2026 (2025).
Membro de associação. ACM.
2021/09/20 - Presente. Orientação. Coping with shared mutable state in a type-state oriented concurrent language (PhD). Coorientador.
2025 - 2026. Curso / Disciplina lecionado. Programação Imperativa. Engenharia Informática (Licenciatura). Universidade do Algarve.
2025 - 2026. Curso / Disciplina lecionado. ANÁLISE E MODELAÇÃO DE SISTEMAS . Engenharia Informática. Universidade do Algarve.
2025 - 2026. Curso / Disciplina lecionado. LABORATÓRIO DE ENGENHARIA DE SOFTWARE . Engenharia Informática (Licenciatura). Universidade do Algarve.
2024/05/20 - 2025/04/04. Organização de evento. 40th ACM/SIGAPP Symposium On Applied Computing. Co-chair of Programming Languages Track.
April 2025, Catania, Italy (2024).
April 2025, Catania, Italy (2024).
2024/03 - 2024/06. Orientação. A DSL for rapid prototyping of consensus algorithms -- Theory.Mestrado em Engenharia Informática (Mestrado). Coorientador.
2024/03 - 2024/06. Orientação. A DSL for rapid prototyping of consensus algorithms -- Implementation.Mestrado em Engenharia Informática (Mestrado). Coorientador.
Membro de associação. ACM SIGAPP .
2024/04/08 - 2024/04/12. Organização de evento. 39th ACM/SIGAPP Symposium On Applied Computing. Co-chair of Programming Languages Track.
April 2024, Avila, Spain (2024).
April 2024, Avila, Spain (2024).
2022. Júri de grau académico. Automatic detection and
resolution of deadlocks in go
programs. Jorge Gabriel Grave Coelho (Mestrado). Universidade Nova de Lisboa Laboratório para a Ciência da Computação e Informática.
resolution of deadlocks in go
programs. Jorge Gabriel Grave Coelho (Mestrado). Universidade Nova de Lisboa Laboratório para a Ciência da Computação e Informática.
2019/10 - 2021/03/31. Orientação. Coping with the reality: adding crucial features to a typestate-oriented language.Mestrado em Engenharia Informática (Mestrado). Coorientador.
2020 - 2021. Orientação. A Framework for Specification and Simulation of Consensus Protocols - http://hdl.handle.net/10362/169642.mestrado em engenharia informatica (Mestrado). Coorientador.
2018 - 2018/01/10. Orientação. Solução Mobile - Banking Pagamentos.Mestrado em Engenharia Informática (Mestrado). Coorientador.
2017 - 2018. Curso / Disciplina lecionado. Teoria da Computacão (Regente). Engenharia Informática (Mestrado). Universidade de Lisboa Faculdade de Ciências.
2016. Júri de grau académico. Behavioral type inference for concurrent object-oriented languages.. Arguente principal. Claudio Jose Albino de Vasconcelos (Mestrado). Universidade Nova de Lisboa Laboratório para a Ciência da Computação e Informática.
2015 - 2016. Curso / Disciplina lecionado. Paradigmas da Programacão (Regente). Engenharia Informática (Licenciatura). Universidade Autónoma de Lisboa.
2015 - 2016. Curso / Disciplina lecionado. Lógica Computacional (Regente). Engenharia Informática (Licenciatura). Universidade da Beira Interior.
2015 - 2016. Curso / Disciplina lecionado. Programação Orientada a Objectos (Regente). Engenharia Informática (Licenciatura). Universidade Autónoma de Lisboa.
2015. Apresentação oral de trabalho. Theory and practice of software analysis (Invited Talk). Instituto Gulbenkian de Ciência (Portugal).
2014 - 2015. Curso / Disciplina lecionado. Programação II (Regente). Engenharia Informática (Licenciatura). Universidade da Beira Interior.
2014 - 2015. Curso / Disciplina lecionado. Programação (Regente). Ciências Biomédicas (Licenciatura). Universidade da Beira Interior.
2014. Júri de grau académico. Tools and Techniques for the Static Verification of Progress in Communication-Centred Systems. Arguente principal. Andre Filipe Marinhas Henriques da Silva Camacho. (Mestrado). Universidade de Lisboa Laboratório de Sistemas Informáticos de Grande Escala.
2012. Apresentação oral de trabalho. Programming secrecy in untrusted networks (Invited Talk). Instituto Superior Tecnico.
2012. Apresentação oral de trabalho. Programming secrecy in untrusted networks (Invited Talk). LSV, École normale supérieure de Cachan (França).
2011. Apresentação oral de trabalho. A linear type system for the pi-calculus (Invited Talk). Behavioural Types Workshop. Universidade Nova de Lisboa.
2010. Apresentação oral de trabalho. A linear type system for the pi-calculus (Invited Talk). INRIA Grenoble-Rhone Alpes.
Projetos
Projetos
2023/01/03 - Presente. Smart Types and Smart Virtual Machines for Validated Smart Contracts (SMARTY). Co-Investigador Responsável (Co-IR). Universidade Nova de Lisboa Laboratório para a Ciência da Computação e Informática.
2021/11/04 - Presente. European Research Network on Formal Proofs. Investigador. Universidade Nova de Lisboa Laboratório para a Ciência da Computação e Informática.
2025/01 - 2025/08/17. POST: Protocols, Observabilities and Session Types, EPSRC. Investigador.
2024/01/10 - 2024/12/31. TaRDIS – Trustworthy and Resilient Decentralised Intelligence for Edge Systems.
2018/03/01 - 2023/12/31. Behavioural Application Program Interfaces (BEHAPI). Investigador.
2023/02/15 - 2023/09/30. Quantified Information Flow Control in Cloud Computing Systems. Investigador.
2020/01/07 - 2023/02/14. Rapid prototyping, reasoning and simulation of consensus protocols and algorithms (COPES). Investigador.
2019/03/15 - 2022/02/28. Distributed Data-Centric Concurrency Control (DeDuCe). Investigador. Universidade Nova de Lisboa Laboratório para a Ciência da Computação e Informática.
2019/04/01 - 2020/03/31. PROSE (Provers for Sessions).. Investigador.
2016/03/21 - 2020/03/20. The European research network on types for programming and verification (EUTypes). Investigador.
2018/12/01 - 2019/03/15. Functional ApproaCh Teaching pOrtuguese couRses (FACTOR). Investigador.
2012/10/01 - 2016/10/31. Behavioural Types for Reliable Large-Scale Software Systems (BETTY). Investigador.
2014/03/01 - 2014/09/30. Languages And Tools for Critical rEal-time Systems., NORTE-07-0124-FEDER-000062. Investigador Pós-doutorado. Universidade do Porto Departamento de Ciência de Computadores.
2012/08/01 - 2014/03/15. Liveness, statically: Behavioural Types for Statically Checking Liveness Properties. Investigador Pós-doutorado.
2014/01/01 - 2014/01/01. Modeling and verification of safety-critical software systems. Investigador responsável. Universidade da Beira Interior Departamento de Informática.
2010/01/01 - 2011/01/31. Concurrency, Mobility and Transactions (Comete). Investigador Pós-doutorado.
2013/01/01 - 2013/01/01. Foundations of static deadlock resolution. Investigador responsável. Universidade Nova de Lisboa Laboratório para a Ciência da Computação e Informática.
2008/04/01 - 2009/03/31. Software Engineering for Service-Oriented Overlay Computers (SENSORIA). Investigador Pós-doutorado.
2005/01/01 - 2007/01/06. Models and Types for Security in Mobile Distributed Systems (MyThS). Bolseiro de Doutoramento.
2005/01/01 - 2006/01/01. Abstract interpretation and model checking for the verification of embedded systems . Bolseiro de Doutoramento.
Produções
Marco Giunti; Nobuko Yoshida. 2026. "Type Congruence, Duality and Iso-Recursive Binary Session Types". https://doi.org/10.1007/978-3-032-05291-9_18
Marco Giunti; Nobuko Yoshida. 2025. "Iso-Recursive Multiparty Sessions and their Automated Verification". Trabalho apresentado em ESOP 2025,2025. https://doi.org/10.1007/978-3-031-91118-7_14
Lorenzo Bacchiani; Mario Bravetti; Marco Giunti; João Mota; António Ravara. 2024. "Behavioural Up/down Casting For Statically Typed Languages". https://doi.org/10.4230/LIPICS.ECOOP.2024.5
Giunti, Marco; Paulino, Hervé; Ravara, António. 2023. "Anticipation of Method Execution in Mixed Consistency Systems". Trabalho apresentado em ACM/SIGAPP Symposium On Applied Computing,27 de março, 2023. https://doi.org/10.1145/3555776.3577725
Giunti, Marco; Paulino, Hervé; Ravara, António. 2023. Anticipation of Method Execution in Mixed Consistency Systems - Technical Report. https://arxiv.org/abs/2212.14651
Mota, Joao; Giunti, Marco; Ravara, António. 2023. "On using VeriFast, VerCors, Plural, and KeY to check object usage". Trabalho apresentado em European Conference on Object-Oriented Programming (ECOOP 2023), Seattle, Estados Unidos,17 de julho, 2023. https://doi.org/10.4230/LIPIcs.ECOOP.2023.40
Giunti, Marco; Paulino, Hervé; Ravara, António; Almeida Matos, Ana; Jan Cederquist; João Matos. 2023. "Type qualifier inference and code synthesis for a better data-centric synchronisation experience.". Trabalho apresentado em ICE 2023 - 16th Interaction and Concurrency Experience,19 de junho, 2023.
Paulino, Hervé; Almeida Matos, Ana; Jan Cederquist; Giunti, Marco; João Matos; Ravara, António. 2023. "AtomiS: Data-centric synchronization made practical ". Trabalho apresentado em OOPSLA,21 de outubro, 2023. https://doi.org/10.1145/3622801
Bacchiani, Lorenzo; Bravetti, Mario; Giunti, Marco; Mota, Joao; Ravara, A.. 2023. "Behavioural up/down casting for statically typed languages (ST30)". Trabalho apresentado em 30 Years of Session Types,20 de outubro, 2023.
Paulino, H.; Matos, A.A.; Cederquist, J.; Giunti, M.; Matos, J.; Ravara, A.. 2023. Sound Atomicity Inference for Data-Centric Synchronization. https://doi.org/10.48550/arXiv.2309.05483
Giunti, Marco; Paulino, Hervé; Ravara, António; Almeida Matos, Ana; Jan Cederquist; João Matos. 2022. AtomiS: data-centric concurrency control made simple. https://doi.org/10.5281/zenodo.6346648
Bacchiani, Lorenzo; Bravetti, Mario; Giunti, Marco; Mota, João; Ravara, António. 2022. "A Java typestate checker supporting inheritance". Science of Computer Programming, 221. https://doi.org/10.1016/j.scico.2022.102844
Mota, João; Giunti, Marco; Ravara, António. 2022. On using VeriFast, VerCors, Plural, and KeY to check object usage. https://arxiv.org/abs/2209.05136
Giunti, Marco; Paulino, Hervé; Ravara, António; Almeida Matos, Ana; Jan Cederquist; João Matos. 2022. AtomiS-Coq : soundness of inference of atomicities . Artifact #61 has been accepted by the ECOOP 2022 Artifact Evaluation program committee
Giunti, M.; Paulino, H.; Ravara, A.. 2022. Anticipation of Method Execution in Mixed Consistency Systems – Technical Report. https://doi.org/10.48550/arXiv.2212.14651
Giunti, Marco; Ravara, António; Mota, João. 2021. "Java Typestate Checker". Trabalho apresentado em International Conference on Coordination Languages and Models (COORDINATION),2021, 121-133. https://doi.org/10.1007/978-3-030-78142-2_8
Giunti, Marco. 2020. "GoPi: Compiling Linear and Static Channels in Go". Em International Conference on Coordination Languages and Models COORDINATION 2020, 137-152.: Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-030-50029-0_9
Giunti, Marco. 2019. The GoPi compiler. https://github.com/marcogiunti/gopi
Giunti, Marco. 2019. A mechanized proof of correctness of the Horn algorithm. https://release.di.ubi.pt/factor/pdfs/A_mechanized_proof_of_correctness_of_the_Horn_algorithm.pdf
Giunti, Marco. 2019. Rewinding functions through CPS . https://release.di.ubi.pt/factor/pdfs/rewind_exp_report.pdf
Giunti, Marco. 2019. "Compiling linear and static channels in Go.". Trabalho apresentado em INFORUM,2019.
GIUNTI, MARCO; VASCONCELOS, VASCO THUDICHUM. 2016. "Linearity, session types and the Pi calculus". Mathematical Structures in Computer Science, 26 (2): 206-237. https://doi.org/10.1017/s0960129514000176
Giunti, Marco; Adrian Francalanza; Antonio Ravara. 2015. "Unlocking Blocked Communicating Processes". Em 11th International Workshop on Automated Specification and Verification of Web Systems (WWV 2015), 23-32.: EPTCS. https://doi.org/10.4204/EPTCS.188.4
Giunti, Marco. 2014. "Static Semantics of Secret Channel Abstractions". Em Nordic Conference on Secure IT Systems NordSec 2014, 165-180.: Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-319-11599-3_10
Giunti, M.; Ravara, A.. 2014. "Towards static deadlock resolution in the p-calculus". https://doi.org/10.1007/978-3-319-05119-2_9
Giunti, Marco; Antonio Ravara. 2013. "Towards Static Deadlock Resolution in the pi-Calculus". Em International Symposium on Trustworthy Global Computing TGC 2013: .: Springer, Berlin, Heidelberg.
Giunti, Marco. 2013. "Algorithmic type checking for a pi-calculus with name matching and session types". The Journal of Logic and Algebraic Programming, 82 (8): 263-281. https://doi.org/10.1016/j.jlap.2013.05.003
Giunti, Marco; Catuscia Palamidessi; Frank D. Valencia. 2012. "Hide and New in the Pi-Calculus". Em EXPRESS/SOS 2012, 65-79.: EPTCS .
Giunti, M.; Palamidessi, C.; Valencia, F.D.. 2012. "Hide and new in the PiCalculus". https://doi.org/10.4204/EPTCS.89.6
Giunti, Marco. 2011. "A type checking algorithm for qualified session types". Em 7th International Workshop on Automated Specification and Verification of Web Systems.: EPTCS. https://doi.org/10.4204/EPTCS.61.7
Giunti, Marco; VASCONCELOS, VASCO THUDICHUM. 2010. "A Linear Account of Session Types in the Pi Calculus". Em CONCUR: International Conference on Concurrency Theory, 432-446.: Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15375-4_30
Giunti, Marco; Honda, Kohei; Vasconcelos, Vasco; Yoshida, Nobuko. 2010. Type safety without subject reduction for session types. http://di.ciencias.ulisboa.pt/~vv/papers/vasconcelos.giunti.etal_type-safety-session-types.pdf
Giunti, Marco; Honda, Kohei; Vasconcelos, Vasco; Yoshida, Nobuko. 2009. "Session-based type discipline for pi calculus with matching". Trabalho apresentado em Programming Language Approaches to Concurrency and Communication-cEntric Software,2009.
Giunti, Marco; Bugliesi, Michele. 2007. "Secure implementations of typed channel abstractions". Em Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '07.: ACM Press. https://doi.org/10.1145/1190216.1190253
Giunti, Marco. 2006. "Preventing intrusions through non-interference". Trabalho apresentado em IEEE Mexican Conference on Informatics Security.,2006.
Giunti, Marco; Bugliesi, Michele. 2005. "Typed Processes in Untyped Contexts". Em International Symposium on Trustworthy Global Computing TGC 2005: , 19-32.: Springer, Berlin, Heidelberg. https://doi.org/10.1007/11580850_3
