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

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. .
  • 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. .
  • 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. .
  • 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. .
  • 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. .
  • Arrial, V., Guerrieri, G., & Kesner, D. (2024). Genericity Through Stratification. Retrieved from http://arxiv.org/abs/2401.12212v2
    Preprint.

2023

  • Accattoli, B., Guerrieri, G., & Leberle, M. (2023). Strong Call-by-Value and Multi Types. Retrieved from http://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. .
  • 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. .
  • 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. .

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. .
  • Accattoli, B., & Guerrieri, G. (2022). The Theory of Call-by-Value Solvability (long version). Retrieved from http://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. .
  • 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. .

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. .
  • 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. .
  • Faggian, C., & Guerrieri, G. (2021). Factorization in Call-by-Name and Call-by-Value Calculi via Linear Logic (long version). Retrieved from http://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. .
  • 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. .
  • 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. .

2020

  • Guerrieri, G., Pellissier, L., & Falco, L. T. D. (2020). Gluing resource proof-structures: inhabitation and inverting the Taylor expansion. Retrieved from http://dx.doi.org/10.46298/lmcs-18(2:4)2022
    Preprint.
  • Lago, U. D., Guerrieri, G., & Heijltjes, W. (2020). Decomposing Probabilistic Lambda-calculi. Retrieved from http://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. .
  • 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. .

2019

  • Guerrieri, G., Pellissier, L., & Falco, L. T. D. (2019). Glueability of resource proof-structures: inverting the Taylor expansion (long version). Retrieved from http://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. .
  • 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. .
  • Accattoli, B., Condoluci, A., Guerrieri, G., & Coen, C. S. (2019). Crumbling Abstract Machines. Retrieved from http://arxiv.org/abs/1907.06057v1
    Preprint.
  • Guerrieri, G., & Manzonetto, G. (2019). The bang calculus and the two Girard鈥檚 translations. In Electronic Proceedings in Theoretical Computer Science Eptcs Vol. 292 (pp. 15-30). doi:10.4204/EPTCS.292.2
    Conference publication. .
  • Guerrieri, G., & Naibo, A. (2019). Postponement of raa and Glivenko鈥檚 Theorem, Revisited. Studia Logica, 107(1), 109-144. doi:10.1007/s11225-017-9781-5
    Article. .
  • Accattoli, B., Guerrieri, G., & Leberle, M. (2019). Types by Need (Extended Version). Retrieved from http://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. .
  • 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. .
  • 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. .
  • 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. .

2018

  • Guerrieri, G. (2018). Towards a Semantic Measure of the Execution Time in Call-by-Value lambda-Calculus (Long Version). Retrieved from http://arxiv.org/abs/1812.10799v1
    Preprint.
  • Accattoli, B., & Guerrieri, G. (2018). Types of Fireballs (Extended Version). Retrieved from http://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. .

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. .
  • Guerrieri, G., & Naibo, A. (2017). Postponement of raa and Glivenko's theorem, revisited (extended version). Retrieved from http://arxiv.org/abs/1710.08854v2
    Preprint.
  • Accattoli, B., & Guerrieri, G. (2017). Implementing Open Call-by-Value (Extended Version). Retrieved from http://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. .

2016

  • Guerrieri, G., Paolini, L., & Rocca, S. R. D. (2016). Standardization and Conservativity of a Refined Call-by-Value lambda-Calculus. Retrieved from http://dx.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. .
  • Accattoli, B., & Guerrieri, G. (2016). Open Call-by-Value (Extended Version). Retrieved from http://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. .
  • 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. .

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

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