Margherita's Publications

Selected Publications (for the full list see my CV)

Mathematical Logic and Foundations of Computer Science

1. [BZ26] R. Borsetto, M. Zorzi. Metatheory of the Modal Logic S4.2 in the Agda Proof Assistant. Journal Paper, submitted.

2. [BZ25b] R. Borsetto, M. Zorzi. NAMOR: a New Agda Library for Modal Extended-Sequents, in proceedings of OVERLAY 25, to appear, 2025.

3. [BZ25a] R. Borsetto, M. Zorzi. An Agda Implementation of the Modal Logic S4.2: first investigations, ICTCS, to appear, 2025. Download here  

4. [PPRZ24] L. Paolini, M. Palazzo, L. Roversi, M. Zorzi Host-Core Calculi for Non-classical Computations: A First Insight. ICTCS 2024: 255-268

5. [MMZ24] S. Martini, A. Masini, M. Zorzi. A natural deduction calculus for S4.2, Notre Dame Journal of Formal Logic, 65(2), 127-150, 2024. doi:https://dx.doi.org/10.1215/00294527-2024-0011.

6. [M M Z 23] S. Martini, A. Masini, M. Zorzi. Cut elimination theorem for ex- tended modal 2-sequents, Bulletin of the Section of Logic Volume 52/4 (2023), pp. 459–495, https://doi.org/10.18778/0138-0680.2023.22.

7. [GMZ23] S. Guerrini, A. Masini, M. Zorzi. Natural deduction calculi for classical and intuitionistic S5, Journal of Applied Non-Classical Logics, Volume 33 - Issue 2, pp. 165-205, 2023.

8. [MMZ20] S. Martini, A. Masini, M. Zorzi, From 2–Sequents and Linear Nested Sequents to Natural Deduction for Normal Modal Logics, ACM Trans. Comput. Log. 22(3): 19:1-19:29 (2021), DOI https://doi.org/10.1145/3461661.

9. [MZ19] M. Zorzi. Quantum Calculi. From Theory to Language Design. Applied Sciences, 9(24), art.number, 5472; pp 1–19, 2019.
   ISSN 2076-3417, DOI https://doi.org/10.3390/app9245472.

10. PRZ19] L. Paolini, L. Roversi, M. Zorzi Quantum Programming Made Easy, Proceedings Joint International Workshop on Linearity and Trends in Linear Logic and Applications, FLOC Conference, Oxford, 7-8 July, 2018, Electronic Proceedings in Theoretical Computer Science (EPTCS) 292, 2019, pp. 133-147, OPA.
    ISSN 2075-2180, DOI 10.4204/EPTCS.292.8

11. [MZ18] A. Masini, M. Zorzi. A logic for quantum register measurements, Axioms, 8 (1), 25, pp.1–10, 2019.
    ISSN 2075-1680, DOI https://doi.org/10.3390/axioms8010025.

12. [P P Z 19] L. Paolini, M. Piccolo, M. Zorzi. qPCF: higher-order languages and quantum circuits, Journal of Automated Reasoning 63(4), pp. 941-966, Springer, 2019.
    Print ISSN 0168-7433, Online ISSN 1573-0670,
    DOI https://doi.org/10.1007/s10817-019-09518-y.

13. [PZ17] L. Paolini, M. Zorzi, qPCF: a Language for Quantum Circuit Computations, in proceedings of Theory and Applications of Models of Computation 14th Annual Conference, TAMC 2017, Bern, Switzerland, April 20-22, 2017, Lecture Notes in Computer Science 10185, pp. 455-469, Springer, 2017. ISBN: 978-3-319-55911-7
    ISSN: 03029743
    DOI: 10.1007/978-3-319-55911-7 33

14. [V V Z17] M. Volpe, L. Viganò, M. Zorzi, A branching distributed temporal logic for reasoning about entanglement-free quantum state transformations. Information&Computation, Volume 255, Part 2, pp 311-333, 2017.
    ISSN 0890-5401, DOI: 10.1016/j.ic.2017.01.007

15. [AZ16] F. Aschieri, M. Zorzi, On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand’s theorem. Theoretical Computer Science, Vol. 625, supplement C, pp. 125–146, 2016. ISSN: 0304-3975, DOI: 10.1016/j.tcs.2016.02.028

16. [MZ16] M. Zorzi, On Quantum Lambda Calculi: a Foundational Perspective. Mathematical Structures in Computer Science, Volume 26, Issue 7, pp. 1107- 1195, Cambridge University Press, 2016.
    ISSN: 0960-1295 (Print), 1469-8072 (Online),
    DOI: http://dx.doi.org/10.1017/S0960129514000425

17. [DZ15] U. Dal Lago, M. Zorzi, Wave-style Token Machine and Quantum Lambda Calculi.
    Post-Proceedings of Third International Workshop on Linearity (LINEARITY 2014) part of VSL-FLoC’14, Vienna, Austria, 13th July, 2014, Electronic Pro- ceedings in Theoretical Computer Science 176, pp. 64-78, OPA, 2015.
    ISSN: 2075-2180
    DOI: 10.4204/EPTCS.176

18. [V V Z14] M. Volpe, L. Viga, M. Zorzi, Quantum State Transformations and Branching Distributed Temporal Logic. In proceedings of 21st International Work- shop on Logic, Language, Information and Computation (Wollic’14), (U. Kohlen- bach, P. Barcel ́o, R. de Queiroz Eds.), Valpara ́ıso, Chile, September 1-4, 2014, Lecture Notes in Computer Science, Vol. 8652, 1–19, Springer, 2014.
    ISBN: 978-3-662-44145-9
    ISSN: 03029743
    DOI: 10.1007/978-3-662-44145-9 1

19. [AZ14] F. Aschieri, M. Zorzi, A “Game Semantical” Intuitionistic Realizability Validating Markov’s Principle. Post-proceedings of 19th International Con- ference on Types for Proofs and Programs (TYPES 2013) 22-26 April 2013, Toulouse, France, Leibniz International Proceedings in Informatics (LIPics), Vol. 26, Pages 24-44, published by Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2014.
    ISBN: 978-3-939897-72-9
    ISSN: 1868-8969
    DOI: 10.4230/LIPIcs.TYPES.2013.24

20. [AZ13] F. Aschieri, M. Zorzi, Non-Determinism, non-termination and the Strong Normalization of System T.
    In proceedings of Typed Lambda Calculi and Applications (TLCA’13), parts of International Conference on Rewriting, Deduction, and Programming, June 23 -28, 2013, Eindhoven (The Netherlands), Lecture Notes in Computer Science LNCS 7941, 31–47. Springer, Heidelberg, 2013.
    ISBN: 978-3-642-38946-7
    ISSN: 0302-9743
    DOI: 10.1007/978-3-642-38946-7 5

21. [AZ12] F. Aschieri, M. Zorzi, Interactive realizability and the elimination of Skolem functions in Peano Arithmetic.
    Proceeding of 4th Classical Logic and Computation - (CL&C’12 Icalp 2012), Warwick - England, 8th July, Electronic Proceedings in Theoretical Computer Science, vol. 97, pp. 1-18, OPA, 2012.
    ISSN 2075-2180DOI 10.4204/EPTCS.97.1

22. [DLZ12] U. Dal Lago, M. Zorzi, Probabilistic Operational Semantics for the Lambda Calculus.
    RAIRO - Theoretical Informatics and Applications, Volume 46, Issue 3, Pages 413-450, 2012.
    Published online by Cambridge University Press. ISSN 0988-3754 (Print), 1290-385X (Online), DOI: http://dx.doi.org/10.1051/ita/2012012.
    
    

23. [DLMZ10b] U. Dal Lago, S. Martini, M. Zorzi, General Ramified Recurrence is Sound for Polynomial Time.
    Proceedings of International Workshop on Developments in Implicit Compu- tational complExity, (DICE 2010, part of ETAPS 2010), march 27-28, 2010, Cyprus. Published in Electronic Proceedings in Theoretical Computer Science, editor P. Baillot, Volume 23, pp. 47-62, OPA, 2010.
    ISSN 2075-2180
    DOI 10.4204/EPTCS.23.4

24. [MV Z11] A. Masini, L. Vigan, M. Zorzi, Modal Deduction Systems for Quantum States Transformations.
    Journal of Multiple-Valued Logic and Soft Computing, Volume 17, Issue 5-6, pp 475-519, Old City Publishing, 2011.
    ISSN 1542-3980 (print), 1542-3999 (online)
    http://www.oldcitypublishing.com/journals/mvlsc-home/mvlsc-issue-contents/mvlsc-volume-17-number-5-6-2011/mvlsc- 17-5-6-p-475-519/

25. [DLMZ11] U. Dal Lago, A. Masini, M. Zorzi, Confluence Results for A Quantum Lambda Calculus with Measurements. Electronic Notes in Theoretical Computer Science, Volume 270, Issue 2, pp. 251-261, Elsevier, 2011.
    ISSN 1571-0661, DOI 10.1016/j.entcs.2011.01.035

26. [DLMZ10] U. Dal Lago, A. Masini, M. Zorzi, Quantum Implicit Computational Complexity. Theoretical Computer Science, Volume 411, Issue 2, pp 377-409, Elsevier, 2010.
    ISSN 0304-3975, DOI 10.1016/j.tcs.2009.07.045

27. [DLMZ09] U. Dal Lago, A. Masini, M. Zorzi, On a Measurement Free Quantum Lambda Calculus with Classical Control. Mathematical Structures in Computer Science, Volume 19, Issue 02, pp 297–335, Cambridge University Press, UK, 2009.
    ISSN 0960-1295 (Print), 1469-8072 (Online), DOI 10.1017/S096012950800741X

28. [MV Z08] A. Masini, L. Vigaòn, M. Zorzi, A Qualitative Modal Representation of Quantum Register Transformations.
    Proceedings of 38th IEEE International Symposium on Multiple Valued Logic (ISMVL 2008), may 22-24, 2008, Dallas TX, USA, editor Gerhard Dueck, pp 131-137, IEEE Computer Society, 2008.
    ISBN 978-0-7695-3155-7 ISSN 0195-623X
    DOI 10.1109/ISMVL.2008.36

APPLIED LOGIC IN COMPUTER SCIENCE AND OTHER TOPICS

In the past I collaborated with some collegues on  AI/Knowledge representation and information systems topics. I've also published some papers about natural language processing (for this categories see my CV).

PhD Thesis

MZPhD09 Lambda Calculi and Logics for Quantum Computing. Ph.D. Thesis, Computer Science Department, Universit`a degli Studi di Verona, 2009.

Master Thesis

 PSL (Parametric Separation Logic), Logica di separazione parametrica, Computer Science Department, Università degli Studi di Verona, 2005.