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 postdoctoral fellow at the Department of Computer Science of the University of Bath (United Kingdom).
Previously, I had been postdoctoral fellow at:

• the Dipartimento di Informatica-Scienza e Ingegneria (DISI) of the Università di Bologna (Italy);
• the Department of Computer Science of the University of Oxford (United Kingdom);
• 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);
• the lab PPS (UMR 7126 of the Univerité Paris Diderot - Paris 7 and CNRS, France).

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

giulio.guerrieri[at]pps.univ-paris-diderot.fr

giulio.guerrieri[at]uniroma3.it

giulio.guerrieri[at]amu-univ.fr

giulio.guerrieri[at]cs.ox.ac.uk

giulio.guerrieri[at]unibo.it

g.guerrieri[at]bath.ac.uk

Office:

4.56, Building 1West

Department of Computer Science, University of Bath

Claverton Down,

Bath BA2 7PB (United Kingdom)

Publications in international journals:

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


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


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


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

Publications in international conferences with review committee:

1. 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).
   pdf (long version) bibtex


2. 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).
   pdf bibtex.


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


4. 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).
   pdf (long version) bibtex.


5. 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).
   pdf (long version) bibtex.


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


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


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


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


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


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


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


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


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


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


17. Categorifying Non-Idempotent Intersection Types (joint work with Federico Olimpieri). To appear in the proceedings of the 29th International Conference Computer Science Logic (CSL 2021), 2021.
    pdf.


18. Factorize Factorization (joint work with Beniamino Accattoli and Claudia Faggian). To appear in the proceedings of the 29th International Conference Computer Science Logic (CSL 2021), 2021.
    pdf.


19. A Deep Quantitative Type System (joint work with Willem Heijltjes and Joseph Paulus). To appear in the proceedings of the 29th International Conference Computer Science Logic (CSL 2021), 2021.
    pdf.


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

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

Teaching:

Year 2020/21:

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