Foundations of Software Systems (FoSS)

Giulio Guerrieri

2025

  • Accattoli, B., Belo Lourenço, C., Ghica, D. R., Guerrieri, G., & Sacerdoti Coen, C. (2025). Closure Conversion, Flat Environments, and the Complexity of Abstract Machines. In Proceedings of the 27th International Symposium on Principles and Practice of Declarative Programming Ppdp 2025 Co Located with the 41st International Conference on Logic Programming. doi:10.1145/3756907.3756922
    Conference publication. View online.
  • Accattoli, B., Ghica, D., Guerrieri, G., Lourenço, C. B., & Coen, C. S. (2025). Closure Conversion, Flat Environments, and the Complexity of Abstract Machines. Retrieved from https://arxiv.org/abs/2507.15843v1
    Preprint.
  • Benedikt, M., Zimmermann, F., Auchmann, B., Bartmann, W., Burnet, J. P., Carli, C., . . . Ballarino, A. (2025). Future Circular Collider Feasibility Study Report: Volume 3 Civil Engineering, Implementation and Sustainability. European Physical Journal Special Topics. doi:10.1140/epjs/s11734-025-01958-5
    Article. View online.

2024

  • Arrial, V., Guerrieri, G., & Kesner, D. (2024). Genericity through stratification. In LICS '24: Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science Vol. 395 (pp. 1-15). Tallinn, Estonia: ACM. doi:10.1145/3661814.3662113
    Conference publication. View on figshare.
  • Kesner, D., Arrial, V., & Guerrieri, G. (2024). Meaningfulness and genericity in a subsuming framework. In Leibniz International Proceedings in Informatics, LIPIcs Vol. 299 (pp. 1:1-1:24). Tallinn, Estonia: Schloss Dagstuhl. doi:10.4230/LIPIcs.FSCD.2024.1
    Conference publication. View on figshare.
  • Arrial, V., Guerrieri, G., & Kesner, D. (2024). The benefits of diligence. In Automated Reasoning. IJCAR 2024. Lecture Notes in Computer Science Vol. 14740 (pp. 338-359). Cham, Switzerland: Springer Nature Switzerland. doi:10.1007/978-3-031-63501-4_18
    Conference publication. View on figshare.
  • Guerrieri, G., Manara, G., de Falco, L. T., & Auclair, L. V. (2024). Confluence for proof nets via parallel cut elimination. In EPiC Series in Computing Vol. 100 (pp. 464-483). Port Louis, Mauritius: EasyChair. doi:10.29007/vkfn
    Conference publication. View on figshare.
  • Acclavio, M., Curzi, G., & Guerrieri, G. (2024). Infinitary cut-elimination via finite approximations. In Leibniz International Proceedings in Informatics, LIPIcs Vol. 288 (pp. 8:1-8:19 pages). Naples, Italy: Schloss Dagstuhl. doi:10.4230/LIPIcs.CSL.2024.8
    Conference publication. View on figshare.
  • Arrial, V., Guerrieri, G., & Kesner, D. (2024). Genericity Through Stratification. Retrieved from https://arxiv.org/abs/2401.12212v2
    Preprint.

2023

  • Accattoli, B., Guerrieri, G., & Leberle, M. (2023). Strong Call-by-Value and Multi Types. Retrieved from https://arxiv.org/abs/2309.12261v1
    Preprint.
  • Faggian, C., Guerrieri, G., Liguoro, U. D., & Treglia, R. (2022). On reduction and normalization in the computational core. Mathematical Structures in Computer Science, 32(7), 934-981. doi:10.1017/S0960129522000433
    Article. View on figshare.
  • Arrial, V., Guerrieri, G., & Kesner, D. (2023). Quantitative inhabitation for different lambda calculi in a unifying framework. Proceedings of the ACM on Programming Languages, 7(POPL), 1483-1513. doi:10.1145/3571244
    Article. View on figshare.
  • Accattoli, B., Guerrieri, G., & Leberle, M. (2023). Strong Call-by-Value and Multi Types. In Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics Vol. 14446 LNCS (pp. 196-215). doi:10.1007/978-3-031-47963-2_13
    Conference publication. View online.

2022

  • Accattoli, B., & Guerrieri, G. (2022). The theory of call-by-value solvability. Proceedings of the ACM on Programming Languages, 6(ICFP), 855-885. doi:10.1145/3547652
    Article. View on figshare.
  • Accattoli, B., & Guerrieri, G. (2022). The Theory of Call-by-Value Solvability (long version). Retrieved from https://arxiv.org/abs/2207.08697v1
    Preprint.
  • Faggian, C., & Guerrieri, G. (2022). Strategies for Asymptotic Normalization. In Leibniz International Proceedings in Informatics Lipics Vol. 228. doi:10.4230/LIPIcs.FSCD.2022.17
    Conference publication. View online.
  • Guerrieri, G., Pellissier, L., & De Falco, L. T. (2022). Gluing resource proof-structures: inhabitation and inverting the Taylor expansion. Logical Methods in Computer Science, 18(2), pages. doi:10.46298/lmcs-18(2:4)2022
    Article. View on figshare.

2021

  • Acclavio, M., & Guerrieri, G. (2021). A deep inference system for differential linear logic. In Electronic Proceedings in Theoretical Computer Science, EPTCS Vol. 353 (pp. 26-49). Open Publishing Association. doi:10.4204/EPTCS.353.2
    Conference publication. View on figshare.
  • Faggian, C., & Guerrieri, G. (2021). Factorization in call-by-name and call-by-value calculi via linear logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Vol. 12650 (pp. 205-225). Springer International Publishing. doi:10.1007/978-3-030-71995-1_11
    Conference publication. View on figshare.
  • Faggian, C., & Guerrieri, G. (2021). Factorization in Call-by-Name and Call-by-Value Calculi via Linear Logic (long version). Retrieved from https://arxiv.org/abs/2101.08364v1
    Preprint.
  • Guerrieri, G., Heijltjes, W. B., & Paulus, J. W. N. (2021). A deep quantitative type system. In Leibniz International Proceedings in Informatics Lipics Vol. 183. doi:10.4230/LIPIcs.CSL.2021.24
    Conference publication. View online.
  • Accattoli, B., Faggian, C., & Guerrieri, G. (2021). Factorize factorization. In Leibniz International Proceedings in Informatics Lipics Vol. 183. doi:10.4230/LIPIcs.CSL.2021.6
    Conference publication. View online.
  • Guerrieri, G., & Olimpieri, F. (2021). Categorifying non-idempotent intersection types. In Leibniz International Proceedings in Informatics Lipics Vol. 183. doi:10.4230/LIPIcs.CSL.2021.25
    Conference publication. View online.

2020

  • Guerrieri, G., Pellissier, L., & Falco, L. T. D. (2020). Gluing resource proof-structures: inhabitation and inverting the Taylor expansion. Retrieved from https://doi.org/10.46298/lmcs-18(2:4)2022
    Preprint.
  • Lago, U. D., Guerrieri, G., & Heijltjes, W. (2020). Decomposing Probabilistic Lambda-calculi. Retrieved from https://arxiv.org/abs/2002.08392v1
    Preprint.
  • Guerrieri, G., Pellissier, L., & Tortora De Falco, L. (2020). Glueability of resource proof-structures: Inverting the Taylor expansion. In Leibniz International Proceedings in Informatics Lipics Vol. 152. doi:10.4230/LIPIcs.CSL.2020.24
    Conference publication. View online.
  • Dal Lago, U., Guerrieri, G., & Heijltjes, W. (2020). Decomposing Probabilistic Lambda-Calculi. In Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics Vol. 12077 LNCS (pp. 136-156). doi:10.1007/978-3-030-45231-5_8
    Conference publication. View online.

2019

  • Guerrieri, G., Pellissier, L., & Falco, L. T. D. (2019). Glueability of resource proof-structures: inverting the Taylor expansion (long version). Retrieved from https://arxiv.org/abs/1910.07936v1
    Preprint.
  • Accattoli, B., Condoluci, A., Guerrieri, G., & Coen, C. S. (2019). Crumbling abstract machines. In ACM International Conference Proceeding Series. doi:10.1145/3354166.3354169
    Conference publication. View online.
  • Accattoli, B., & Guerrieri, G. (2019). Abstract machines for Open Call-by-Value. Science of Computer Programming, 184. doi:10.1016/j.scico.2019.03.002
    Article. View online.
  • Accattoli, B., Condoluci, A., Guerrieri, G., & Coen, C. S. (2019). Crumbling Abstract Machines. Retrieved from https://arxiv.org/abs/1907.06057v1
    Preprint.
  • Guerrieri, G., & Manzonetto, G. (2019). The bang calculus and the two Girard’s translations. In Electronic Proceedings in Theoretical Computer Science Eptcs Vol. 292 (pp. 15-30). doi:10.4204/EPTCS.292.2
    Conference publication. View online.
  • Guerrieri, G., & Naibo, A. (2019). Postponement of raa and Glivenko’s Theorem, Revisited. Studia Logica, 107(1), 109-144. doi:10.1007/s11225-017-9781-5
    Article. View online.
  • Accattoli, B., Guerrieri, G., & Leberle, M. (2019). Types by Need (Extended Version). Retrieved from https://arxiv.org/abs/1902.05945v1
    Preprint.
  • Accattoli, B., Faggian, C., & Guerrieri, G. (2019). Factorization and normalization, essentially. In Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics Vol. 11893 LNCS (pp. 159-180). doi:10.1007/978-3-030-34175-6_9
    Conference publication. View online.
  • Guerrieri, G., Pellissier, L., & Tortora de Falco, L. (2019). Proof-Net as Graph, Taylor Expansion as Pullback. In Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics Vol. 11541 LNCS (pp. 282-300). doi:10.1007/978-3-662-59533-6_18
    Conference publication. View online.
  • Guerrieri, G. (2019). Towards a semantic measure of the execution time in call-by-value lambda-calculus. In Electronic Proceedings in Theoretical Computer Science Eptcs Vol. 293 (pp. 57-72). doi:10.4204/EPTCS.293.5
    Conference publication. View online.
  • Accattoli, B., Guerrieri, G., & Leberle, M. (2019). Types by Need. In Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics Vol. 11423 LNCS (pp. 410-439). doi:10.1007/978-3-030-17184-1_15
    Conference publication. View online.

2018

  • Guerrieri, G. (2018). Towards a Semantic Measure of the Execution Time in Call-by-Value lambda-Calculus (Long Version). Retrieved from https://arxiv.org/abs/1812.10799v1
    Preprint.
  • Accattoli, B., & Guerrieri, G. (2018). Types of Fireballs (Extended Version). Retrieved from https://arxiv.org/abs/1808.10389v2
    Preprint.
  • Accattoli, B., & Guerrieri, G. (2018). Types of Fireballs. In Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics Vol. 11275 LNCS (pp. 45-66). doi:10.1007/978-3-030-02768-1_3
    Conference publication. View online.

2017

  • Guerrieri, G., Paolini, L., & Rocca, S. R. D. (2017). Standardization and conservativity of a refined call-by-value lambda-calculus. Logical Methods in Computer Science, 13(4), pages. doi:10.23638/LMCS-13(4:29)2017
    Article. View on figshare.
  • Guerrieri, G., & Naibo, A. (2017). Postponement of raa and Glivenko's theorem, revisited (extended version). Retrieved from https://arxiv.org/abs/1710.08854v2
    Preprint.
  • Accattoli, B., & Guerrieri, G. (2017). Implementing Open Call-by-Value (Extended Version). Retrieved from https://arxiv.org/abs/1701.08186v2
    Preprint.
  • Accattoli, B., & Guerrieri, G. (2017). Implementing Open Call-by-Value. In Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics Vol. 10522 LNCS (pp. 1-19). doi:10.1007/978-3-319-68972-2_1
    Conference publication. View online.

2016

  • Guerrieri, G., Paolini, L., & Rocca, S. R. D. (2016). Standardization and Conservativity of a Refined Call-by-Value lambda-Calculus. Retrieved from https://doi.org/10.23638/LMCS-13(4:29)2017
    Preprint.
  • Ehrhard, T., & Guerrieri, G. (2016). The bang calculus: An untyped lambda-calculus generalizing Call-By-Name and Call-By-Value. In Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming Ppdp 2016 (pp. 174-187). doi:10.1145/2967973.2968608
    Conference publication. View online.
  • Accattoli, B., & Guerrieri, G. (2016). Open Call-by-Value (Extended Version). Retrieved from https://arxiv.org/abs/1609.00322v2
    Preprint.
  • Guerrieri, G., Pellissier, L., & De Falco, L. T. (2016). Computing connected proof(-Structure)s from their taylor expansion. In Leibniz International Proceedings in Informatics Lipics Vol. 52. doi:10.4230/LIPIcs.FSCD.2016.20
    Conference publication. View online.
  • Accattoli, B., & Guerrieri, G. (2016). Open call-by-value. In Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics Vol. 10017 LNCS (pp. 206-226). doi:10.1007/978-3-319-47958-3_12
    Conference publication. View online.

2015

  • Guerrieri, G., Paolini, L., & Della Rocca, S. R. (2015). Standardization of a call-by-value lambda-calculus. In Leibniz International Proceedings in Informatics Lipics Vol. 38 (pp. 211-225). doi:10.4230/LIPIcs.TLCA.2015.211
    Conference publication. View online.
  • Guerrieri, G. (2015). Head reduction and normalization in a call-by-value lambda-calculus. In Openaccess Series in Informatics Vol. 46 (pp. 3-17). doi:10.4230/OASIcs.WPTE.2015.3
    Conference publication. View online.

2014

  • Carraro, A., & Guerrieri, G. (2014). A semantical and operational account of call-by-value solvability. In Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics Vol. 8412 LNCS (pp. 103-118). doi:10.1007/978-3-642-54830-7_7
    Conference publication. View online.