Giulio Guerrieri, PhD

I have a PhD in Computer Science and Philosophy. During my PhD I was at the Dipartimento di Filosofia of the Università Roma Tre (Rome, Italy) and in the lab PPS of the Université Paris Diderot - Paris 7 (Paris, France). My PhD supervisors were Lorenzo Tortora de Falco and Thomas Ehrhard.

I am currently a lecturer (= associate professor) in computer science at the Department of Informatics of the University of Sussex in Brighton, United Kingdom.

I am also a Maître de Conférences (= associate professor) in computer science at the Aix-Marseille University (AMU) in France, currently in voluntary layoff status; my research was at the Laboratoire d'Informatique et Systemes (LIS, UMR 7020), in the LSC team at the Luminy campus (Marseille, France); my teaching was at the Institut Universitaire de Technologie (IUT) in Aix-en-Provence.

Previously, I had been a senior researcher at the Programming Language team of the Huawei Edinburgh Research Centre in Edinburgh (United Kingdom).

Before that, I had been postdoctoral fellow at:

• the Department of Computer Science of the University of Bath (United Kingdom), 2019-2021;
• the Dipartimento di Informatica-Scienza e Ingegneria (DISI) of the Università di Bologna (Italy), 2018;
• the Department of Computer Science of the University of Oxford (United Kingdom), 2017;
• the lab I2M (UMR 7373 of the Aix-Marseille Université and CNRS), with a visit to the Dipartimento di Matematica e Fisica (Università Roma Tre, Italy), 2016;
• the lab PPS (UMR 7126 of the Univerité Paris Diderot - Paris 7 and CNRS, France), 2014-2015.

Email: (replace [at] with the email key)

g.guerrieri[at]sussex.ac.uk

giulio.guerrieri[at]lis-lab.fr

giulio.guerrieri[at]univ-amu.fr

Office:

Campus universitaire de Luminy

Building TPR2, Block 1, 4th floor, Room 04.38

163 avenue de Luminy

13288 MARSEILLE cedex 09 (France)

Publications in international journals

1. Quantitative Inhabitation for Different Lambda Calculi in a Unifying Framework (joint work with Victor Arrial and Delia Kesner). Proceedings of the ACM on Programming Languages, Vol. 7, Issue POPL, pp. 1483-1513, 2023.
   pdf bibtex.


2. On Reduction and Normalization in the Computational Core (joint work with Ugo de’Liguoro, Claudia Faggian, Riccardo Treglia). Mathematical Structures in Computer Science, Vol. 37, Issue 7, pp. 934–981, 2022.
   pdf bibtex.


3. The Theory of Call-by-Value Solvability (joint work with Beniamino Accattoli). Proceedings of the ACM on Programming Languages, Vol. 6, Issue ICFP, pp. 855-885, 2022.
   pdf bibtex.


4. Gluing resource proof-structure: inabitation and inverting the Taylor expansion (joint work with Luc Pellissier and Lorenzo Tortora de Falco). Logical Methods in Computer Science (LMCS) (special issue of selected papers of CSL 2020), Vol. 18, Number 2, 2022.
   pdf bibtex.


5. Abstract Machines for Open Call-by-Value (joint work with Beniamino Accattoli). Science of Computer Programming (special issue of selected papers of FSEN 2017), 2019.
   pdf bibtex.


6. Postponement of RAA and Glivenko's theorem, revisited (joint work with Alberto Naibo). Studia Logica (Special issue of General Proof Theory 2015, celebrating 50 Years of Dag Prawitz's "Natural Deduction"), Vol. 107, Number 1, pp. 109-144, 2019.
   pdf pdf (long version) bibtex. Une presentation du travail est disponible ici.


7. Standardization and Conservativity of a Refined Call-by-Value lambda-Calculus (joint work with Luca Paolini and Simona Ronchi Della Rocca). Logical Methods in Computer Science (LMCS) (special issue of selected papers of RTA-TLCA 2015), Vol. 13, Issue 4, 2017.
   pdf bibtex.

Publications in international conferences with review committee

1. Genericity through Stratification (joint work with Victor Arrial and Delia Kesner). To appear in the proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2024), 2024.
   pdf bibtex.


2. The Benefits of Diligence (joint work with Victor Arrial and Delia Kesner). To appear in the proceedings of the International Joint Conference on Automated Reasoning (IJCAR 2024), 2024.
   pdf bibtex.


3. Confluence of Proof-Nets via Parallel Cut-Elimination (joint work with Giulia Manara, Lorenzo Tortora de Falco and Lionel Vaux Auclair). To appear in the proceedings of the 25th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-25), 2024.
   pdf bibtex.


4. Infinitary Cut-Elimination via Finite Approximations (joint work with Matteo Acclavio and Gianluca Curzi). 32th International Conference Computer Science Logic (CSL 2024), 2024.
   pdf bibtex.


5. Strong Call-by-Value and Multi Types (joint work with Beniamino Accattoli and Maico Leberle). 20th International Colloquium on Theoretical Aspects of Computing (ICTAC 2023), 2023.
   pdf bibtex.


6. Strategies for Asymptotic Normalization (joint work with Claudia Faggian). 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), 2022.
   pdf bibtex.


7. A Deep Inference System for Differential Linear Logic (joint work with Matteo Acclavio). Proceedings of the 6th workshop Linearity and of the 4th workshop Trends in Linear Logic and Applications (Linearity/TLLA 2020), 2021.
   pdf bibtex.


8. Factorizing Call-by-Name and Call-by-Value Calculi via Linear Logic (joint work with Claudia Faggian). 24th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2021), 2021.
   pdf bibtex.


9. A Deep Quantitative Type System (joint work with Willem Heijltjes and Joseph Paulus). 29th International Conference Computer Science Logic (CSL 2021), 2021.
   pdf bibtex.


10. Factorize Factorization (joint work with Beniamino Accattoli and Claudia Faggian). 29th International Conference Computer Science Logic (CSL 2021), 2021.
    pdf bibtex.


11. Categorifying Non-Idempotent Intersection Types (joint work with Federico Olimpieri). 29th International Conference Computer Science Logic (CSL 2021), 2021.
    pdf bibtex..


12. Decomposing Probabilistic lambda-Calculus (joint work with Ugo Dal Lago and Willem Heijltjes). 23rd International Conference Foundations of Software Science and Computation Structures (FoSSaCS 2020), 2020.
    pdf bibtex.


13. Glueability of resource proof-structures: inverting the Taylor expansion (joint work with Lorenzo Tortora de Falco and Luc Pellissier). 28th International Conference Computer Science Logic (CSL 2020), 2020.
    pdf bibtex.


14. Factorization and Normalization, Essentially (joint work with Beniamino Accattoli and Claudia Faggian). 17th Asian Symposium on Programming Languages and Systems, (APLAS 2019).
    pdf (long version) bibtex.


15. Crumbling Abstract Machines (joint work with Beniamino Accattoli, Andrea Condoluci and Claudio Sacerdoti Coen). 21st International Symposium on Principles and Practice of Programming Languages (PPDP 2019), 2019.
    pdf (long version) bibtex.


16. Proof-net as graph, Taylor expansion as pullback (joint work with Lorenzo Tortora de Falco and Luc Pellissier). 26th Workshop on Logic, Language, Information and Computation (WoLLIC 2019), 2019.
    pdf bibtex.


17. Types by Need (joint work with Beniamino Accattoli and Maico Leberle). 28th European Symposium on Programming, (ESOP 2019), 2019.
    pdf (long version) bibtex.


18. Towards a Semantic Measure of the Execution Time in Call-by-Value lambda-Calculus. Intersection Types and Related Systems (ITRS 2018), 2019.
    pdf bibtex.


19. The Bang Calculus and the Two Girards's Translations (joint work with Giulio Manzonetto). Trends in Linear Logic and Applications / Linearity (TLLA/Linearity 2018), 2019.
    pdf bibtex.


20. Types of Fireballs (joint work with Beniamino Accattoli). 16th Asian Symposium on Programming Languages and Systems, (APLAS 2018), 2018.
    pdf (long version) bibtex.


21. Implementing Open Call-by-Value (joint work with Beniamino Accattoli). 7th IPM International Conference on Foundamentals of Software Engineering (FSEN 2017), 2017.
    pdf bibtex.


22. Open Call-by-Value (joint work with Beniamino Accattoli). 14th Asian Symposium on Programming Languages and Systems, (APLAS 2016), 2016.
    pdf (a previous version: pdf) bibtex.


23. The bang calculus: an untyped lambda-calculus generalizing Call-By-Name and Call-By-Value (joint work with Thomas Ehrhard). 18th International Symposium on Principles and Practice of Declarative Programming (PPDP 2016), 2016.
    pdf (long version) bibtex.


24. Computing connected proof(-structure)s from their Taylor expansion (joint work with Luc Pellissier and Lorenzo Tortora de Falco). 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), 2016.
    pdf (long version) bibtex.


25. Head reduction and normalization in a call-by-value lambda-calculus. 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015), 2015.
    pdf bibtex.


26. Standardization of a call-by-value lambda-calculus (joint work with Luca Paolini and Simona Ronchi Della Rocca). 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015), 2015.
    pdf bibtex.


27. A semantical and operational account of call-by-value solvability (joint work with Alberto Carraro). 17th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2014), 2014.
    pdf (long version) bibtex

Other works

Preprints, technical reports and submissions:

• Relational type-checking for MELL proof-structures. Part 1: Multiplicatives (joint work with Luc Pellissier and Lorenzo Tortora de Falco), submitted to Intersection Types and Related Systems (ITRS 2016), 2016. pdf.
• Syntax, Taylor expansion and relational semantics of MELL proof-structures: an unusual approach (joint work with Luc Pellissier and Lorenzo Tortora de Falco), technical report technique, 2016, pdf.

Communications at international workshops with program committee (without publication or with informal publication):

• A new point of view on the Taylor expansion of proof-nets and uniformity (joint work with Lorenzo Tortora de Falco), for Linearity 2014 (pdf). A more detailed version is here.
• Injectivity of relational semantics for (connected) MELL proof-nets via Taylor expansion (joint work with Lorenzo Tortora de Falco and Luc Pellissier), for Termgraph 2014 (pdf), and pour TACL 2015 (pdf). A more detailed version (work in progress) is here.

Invited talks in international workshops/conferences with proceedings

1. Third joint workshop Linearity and Trends in Linear Logic and Applications (Linearity & TLLA 2022, affiliated to FSCD 2022), 31 July–1 August 2022, Haifa (Israel).


2. Sixteenth workshop on Logical and Semantic Frameworks with Applications (LSFA 2021, affiliated to FSCD 2021), 23-24 July 2021, Buenos Aires (Argentina).

Program committee member of international workshops/conferences with proceedings

1. Eighteenth International Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2023, affiliated to the international conference FSCD 2023), 1-2 July 2023, Rome (Italy).


2. Thirty-first International Conference Computer Science Logic (CSL 2023), 13-16 February 2023, Warsaw (Poland).


3. Nineteenth Asian Symposium on Programming Languages and Systems (APLAS 2021), 17-22 October 2021 Chicago, Illinois (USA).


4. Fifth Workshop on Trends in Linear Logic and Applications (TLLA 2021, affiliated to the international conference LICS 2021), 27-28 June 2021, Dortmund (Germany).


5. Tenth Workshop on Intersection Types and Related Systems (ITRS 2021, affiliated to the international conference FSCD 2021), 17 July 2021, Buenos Aires (Argentina).


6. Third Workshop on Trends in Linear Logic and Applications (TLLA 2019, affiliated to the international conference FSCD 2019), 29-30 June 2019, Dortmund (Germany).


7. Fifth International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2018, affiliated to the international conference FSCD 2018 and FLOC 2018), 7 July 2018, Oxford (United Kingdom).

Teaching:

Schools:

1. The lambda-calculus: from simple types to non-idempotent intersection types. 34th European Summer School in Logic, Language and Information (ESSLLI 2023). 7-11 August 2023, Ljubljana (Slovenia). Course materials can be found here.


2. The lambda-calculus: from simple types to non-idempotent intersection types. 37th Escuela de Ciencias Informaticás (ECI 2024). 29 July - 2 August 2024, Buenos Aires (Argentina). Course materials can be found here.

Academic:

Year 2020/21:

• Class tutor of "Functional Programming" for the Bachelor's and Master's degrees in Computer Science and Mathematics (University of Bath, United kingdom).
• Class tutor of "Logic and Semantics of Programming Languages" for the Bachelor's and Master's degrees in Computer Science and Mathematics (University of Bath, United kingdom).
• Class tutor of "Foundations of Computation" for the Bachelor's and Master's degrees in Computer Science and Mathematics (University of Bath, United kingdom).

Year 2019/20:

• Class tutor of "Functional Programming" for the Bachelor's and Master's degrees in Computer Science and Mathematics (University of Bath, United kingdom).

Year 2018/19:

• Class tutor of "Functional Programming" for the Bachelor's and Master's degrees in Computer Science and Mathematics (University of Bath, United kingdom).
• Class tutor of "Logic for Computer Science" for the Bachelor's degree in Computer Science (Università di Bologna, Italy).

Year 2017/18:

• Class tutor of "Programming for Mathematics" for the Bachelor's degree in Mathematics (Università di Bologna, Italy).
• Class tutor of "Algorithms and Data Structures" for the Bachelor's degree in Computer Science (Università di Bologna, Italy).
• Class tutor and marker of "Automata, Logic and Games" for the Master's degree in Computer Science (University of Oxford, United Kingdom).
• Class tutor and marker of "Foundations of Computer Science" for the Master's degree in Computer Science (University of Oxford, United Kingdom).

Year 2016/17:

• Lecturer and class tutor of "Introduction to Mathematics" for the Bachelor's degree in Computer Science (Université Paris 1 Panthéon-Sorbonne, semester 1): Friday 14:00-17:00, room C2204, building Pierre Mendès France (Tolbiac).

Year 2015/16 :

• Class tutor of "Logic" for the Bachelor's degree in Philosophy (Université Paris 1 Panthéon-Sorbonne, semester 1): Wednesday 16:00-18:00, room Cavaillès.
  
  
  • course webpage

Year 2014/15:

• Class tutor and marker of "Logic" for the Bachelor's degree in Philosophy (Université Paris 1 Panthéon-Sorbonne, semester 1): Tuesday 16:30-18:30, room Halbwachs.
• Lecturer and class tutor of "Introduction to Computer Science" for the Bachelor's degree in Philosophy (Université Paris 1 Panthéon-Sorbonne, semester 1): Wednesday 14:00-15:30, room C401, building Pierre Mendès France.
  
  
  • course webpage

Year 2013/14:

• Class tutor and marker of "Environments and Development Tools" (ED6) for the Bachelor's degree of Computer Science (Université Paris Diderot - Paris 7, semester 1): every other Monday, 14:30-16:30, room 2032, building Sophie-Germain.
  
  
  • course webpage


• Class tutor and marker of "Logic" (LO6) for the Bachelor's degree in Computer Science (Université Paris Diderot-Paris 7, semester 2): Tuesday 11:00-13:00, room 165, building Olympe de Gouges.
  
  
  • course webpage
  • tutorials webpage


• Class tutor and marker of "Introduction to Computer Science and Programming" (IF1) for the Bachelor's degree in Mathematics (Univerité Paris 7-Paris Diderot, semester 1): Wednesday 8:30-10:30, room 277F, building Halle aux Farines.
  
  
  • course webpage
  • tutorial webpage


• Class tutor and marker of "Functional Programming" (PF5) for the Bachelor's degree in Computer Science (Université Paris Diderot-Paris 7, semester 1): Tuesday 13:30-15:30, room 2031, building Sophie-Germain.
  
  
  • course webpage

Year 2012/13:

• Class tutor and marker of "Introduction to Computer Science and Programming"" (IF1) for the Bachelor'a degree in Mathematics (Université Paris Diderot-Paris 7, semester 1): Thursday 8:30-10:30, room 123C (477F since 25 October), building Halle aux Farines.
  
  
  • la page du cours
  • la page du groupe


• Class tutor and marker of "Logical Tools" (OL3) for the Bachelor's degree in Computer Science (Université Paris Diderot-Paris 7, semester 1): Friday 14:30-16:30, room Script 551C, building Halle aux Farines.
  
  
  • la page du cours


• Class tutor of "Network Programming" for the Bachelor's degree in Computer Science (Université Paris Diderot-Paris 7, semester 2): Thursday 9:00-11:00, room 2032, building Sophie-Germain.
  
  
  • course webpage
  • tutorial webpage

Year 2011/2012

• Class tutor and marker of "Logic" for the Bachelor’s degree in Philosophy (Univ. Paris 1, Panthéon – Sorbonne).

Year 2010/2011

• Class tutor and marker of "Introduction to programming" (IF1), for the Bachelor’s degrees in Computer Science and Mathematics (Univ. Paris Diderot – Paris 7, Paris, France).