Marco Benini

Publications

In preparation

      1. M. Benini, Mathematical Logic – Lecture Notes, book
      2. M. Benini, R. Bonacina, Point-free categorical semantics for Martin-Löf type theory, article
      3. M. Benini, O. Beyersdorff, M. Rathjen, P. Schuster editors, Mathematics for Computation, book
      4. M. Benini, P. Schuster, Fondamenti di Matematica, book
      5. M. Benini, R. Bonacina, The Categorical Structure of Well Quasi Orders, article

Books

      1. F. Gobbo, M. Benini, Constructive Adpositional Grammars: Foundations of Constructive Linguistics, Cambridge Scholar Press (2011) (pdf)
      2. M. Benini, Constructive Analysis and Synthesis of Programs, Lulu.com (2009) (pdf)

Journal articles

      1. M. Benini, R. Bonacina, The Higman’s Lemma in a categorical setting submitted (2016)
      2. F. Gobbo, M. Benini, What Can We Know of Computational Information? The Conceptual Re-Engineering of Measuring, Quantity, and Quality, Topoi 35(1), pp. 203-212 (2016). Published online since 2014.
      3. F. Gobbo, M. Benini, Why zombies can’t write significant source code: The Knowledge Game and the Art of Computer Programming, Journal of Experimental & Theoretical Artificial Intelligence 27(1), pp. 37-50 (2015)
      4. F. Gobbo, M. Benini, The Minimal Levels of Abstraction in the History of Modern Computing,  Philosophy & Technology 27(3), pp. 327-343 (2014)
      5. F. Gobbo, M. Benini, From Ancient to Modern Computing: A History of Information Hiding, IEEE Annals of the History of Computing 35(3), pp. 33-39 (2013)
      6. M. Benini, La nozione di spazio in Matematica, Il Protagora, anno XL, gennaio-giugno, sesta serie, n.19, pp. 43-73 (2013) (pdf)
      7. M. Benini, S. Sicari, Dealing with the security behaviour of large scale systems, Journal of Information Assurance and Security, 7(3), pp. 229-240 (2012). (pdf)
      8. M. Benini, S. Sicari, A Mathematical Derivation of a Risk Assessment Procedure, IAENG International Journal of Applied Mathematics, 40(2), pp. 52-62 (2010) (pdf)
      9. M. Benini, S. Sicari, Risk Assessment via Partial Orders, Advances in Computer Science and Engineering 3(1), pp. 19-46 (2009). (pdf)
      10. M. Benini, S. Sicari, Risk Assessment in Practice: A Real Case Study, Computer Communications 31(15), pp. 3691-3699 (2008) (pdf)
      11. M. Benini, S. Sicari, Assessing the risk to intercept VoIP calls, Journal of Computer Networks 52(12), pp. 2432-2446 (2008) (pdf)
      12. M. Ornaghi, M. Benini, M. Ferrari, C. Fiorentini, A. Momigliano, A Constructive Object Oriented Modeling Language for Information Systems, Electronic Notes in Theoretical Computer Science 153(1), pp. 55-75 (2006) (pdf)
      13. M. Acquaviva, M. Benini, Strategie adattive nei web-based learning systems: un approccio comparativo, WBT.it (2006) [electronic magazine] (pdf)
      14. M. Acquaviva, M. Benini, Towards Short Term Content Adaptation, eWiC – BCS (2005) [electronic magazine] (pdf)
      15. M. Acquaviva, M. Benini, VICE: E-Learning nell’era del Semantic Web, WBT.it (2005) [electronic magazine]. (pdf)
      16. A. Avellone, M. Benini, U. Moscato, How to Avoid the Verification of a Theorem Prover, Logical Journal of the IGPL 9(1), pp. 7-31 (2001) (pdf)
      17. M. Benini, Strong Constructivity of Second Order Intuitionistic Arithmetic, Journal of Symbolic Logic Bullettin (1999) [abstract] (pdf)
      18. G. Degli Antoni, D. Cabianca, F. Casablanca, M. Benini, M. Vaccari, Linearity of Client/Server Systems, European Association on Theoretical Computer Science Bullettin 57 (1995) (pdf)

Book chapters and proceedings

      1. M. Benini, R. Bonacina, Kruskal’s Variations submitted (2017)
      2. M. Benini, Proof-Oriented Categorical Semantics, in D. Probst,  P. Schuster eds., Concepts of Proof in Mathematics, Philosophy, and Computer Science, Ontos Mathematical Logic 6, De Gruyter, pp. 41-68 (2016)
      3. M. Benini, F. Gobbo, Algorithms and their explanations, in A. Beckmann, E. Csuhaj-Varju, and K. Meer eds., CiE 2014, Lecture Notes in Computer Science 8493,  Springer-Verlag, pp. 32-41 (2014)
      4. F. Gobbo, M. Benini, From Structural Syntax to Constructive Adpositional Grammars, in K. Gerdes, E. Hajičová, L. Wanner eds., Computational Dependency Theory, Frontiers in Artificial Intelligence and Application 258, IOS Press, pp. 113-135 (2014)
      5. M. Benini, S. Sicari, A Mathematical Framework for Risk Assessment, in H. Labiod, M. Badra eds., New Technologies, Mobility and Security, Springer, pp. 459-470 (2007)
      6. M. Acquaviva, M. Benini, A. Trombetta, A Model for Short Term Content Adaptation, in WWW ’05 Special interest tracks and posters of the 14th international conference on World Wide Web, ACM Press, pp. 1034-1035 (2005)
      7. M. Benini, F. De Cindio, L. Sonnante, Virtuose, a VIRTual CommUnity Open Source Engine for integrating civic networks and digital cities, in P. van den Besselaar, S. Koizumi eds., Digital Cities III. Information Technologies for Social Capital: Cross-cultural Perspectives, Lecture Notes in Computer Science 3081, Springer-Verlag, pp. 217-232 (2005)
      8. M. Benini, Representing Object Code, in J.Lloyd, V. Dahl, U. Furbach, M. Kerber, K.-K. Lau, C. Palamidessi, L.M. Pereira, Y. Sagiv, P.J. Stuckey eds., Computational Logic – CL 2000: First International Conference London, UK, July 24-28, 2000 Proceedings, Lecture Notes in Artificial Intelligence 1861, Springer-Verlag, pp. 538-552 (2000)
      9. M. Benini, D. Nowotka, C. Pulley, Computer Arithmetic: Logic, Calculation and Rewriting,  in D. M. Gabbay, M. De Rijke eds., Frontiers of Combining Systems 2, Studies in Logic and Computation, Research Studies Press, 2nd edition (2000) (pdf)
      10. M. Benini, S. Kalvala, D. Nowotka, Program Abstraction in a Higher Order Logic Framework,  in J. Grundy, M. Newey, Theorem Proving in Higher Order Logics: 11th International Conference, TPHOLs’98, Canberra, Australia, September 27 – October 1, 1998, Proceedings, Lecture Notes in Computer Science 1479, Springer-Verlag, pp. 33-48 (1998) (pdf)

Conferences

      1. M. Benini, Well Quasi Orders in a Categorical SettingWell-quasiorderings: From Theory to Applications symposium at Jahrestagung der Deutschen Mathematiker-Vereinigung (2015)
      2. M. Benini, Proof-Theoretic Semantics: Point-free meaning of first-order systems, Trends in Proof Theory workshop at Jahrestagung der Deutschen Mathematiker-Vereinigung (2015)
      3. M. Benini, Does programming really need data structures?, CORCON 2014, Correcteness by Construction (2014) (pdf)
      4. M. Benini, F. Gobbo, Algorithms and their explanations, CiE 2014, special session History and Philosophy of Computing. In A. Beckmann, E. Csuhaj-Varju, and K. Meer (Eds.), CiE 2014, LNCS 8493, pp. 32-41, Springer (2014)
      5. M. Benini, F. Gobbo, The epistemology of programming language paradigms, HAPOC (2013) (pdf)
      6. M. Benini, F. Gobbo, Measuring Computational Complexity: the Qualitative and Quantitative Intertwining of Algorithm Comparison, Fifth Workshop on the Philosophy of Information (2013) (pdf)
      7. F. Gobbo, M. Benini, What Can We Know of Computational Inforgs?, Fifth Workshop on the Philosophy of Information (2013) (pdf)
      8. F. Gobbo, M. Benini, From Computing Machineries to Cloud Computing: The Minimal Levels of Abstraction of Inforgs through History, HAPOC (2011) (pdf)
      9. F. Gobbo, M. Benini, From Structural Syntax to Constructive Adpositional Grammars, Depling (2011). Also in K. Gerdes, E. Hajičová, L. Wanner (Eds.), Computational Dependency Theory, Frontiers in Artificial Intelligence and Application 258, pp. 113-135, IOS Press (2013) (pdf)
      10. F. Gobbo, M. Benini, A Constructive Mathematics approach for Natural Language formal grammars, Computing and Philosophy, E-CAP (2009) (pdf)
      11. M. Benini, S. Sicari, Towards More Secure Systems: How to Combine Expert Evaluations, SecureComm (2008) (pdf)
      12. M. Benini, S. Sicari, A Power Conservative Underwater Localization Algorithm, IEEE Gold (2008). (pdf)
      13. M. Benini, F. Gobbo, Virtual Communities as Narrative Processes, C&T- Workshop Between Ontologies and Folksonomies (2007) (pdf)
      14. M. Benini, S. Sicari, A Mathematical Framework for Risk Assessment, NTMS2007 (2007) (pdf)
      15. M. Benini, S. Sicari, Risk Assessment: Intercepting VoIP Calls, V-IPSI 2007 Venice (2007) (pdf)
      16. M. Acquaviva, M. Benini, Strategie adattive nei web-based learning systems: un approccio comparativo, EXPO E-Learning 05 (2005). Also available as an electronic magazine article, see above (pdf)
      17. M. Acquaviva, M. Benini, Adaptive Strategies in Web-Based Learning Systems: A Comparative Survey, INTERACT2005 (2005) (pdf)
      18. M. Acquaviva, M. Benini, A. Trombetta, Short-Term Content Adaptation in Web-Based Learning Systems, WTAS2005 (2005) (pdf)
      19. M. Acquaviva, M. Benini, A. Trombetta, A Model for Short Term Content Adaptation, WWW2005 (2005) (pdf)
      20. M. Acquaviva, M. Benini, Towards Short Term Content Adaptation, First ELeGI Int. Conf. on Advanced Technology for Enhanced Learning (2005). Also available as an electronic magazine article, see above (pdf)
      21. M. Acquaviva, M. Benini, VICE: E-Learning nell’era del Semantic Web, EXPO E-Learning 04 (2004). Also available as an electronic magazine article, see above (pdf)
      22. M. Benini, F. De Cindio, L. Sonnante, Virtuose, a VIRTual CommUnity Open Source Engine for integrating civic networks and digital cities, C&T- Workshop Digital Cities (2003) (pdf)
      23. M. Benini, Representing Object Code, CL2000 (2000) (pdf)
      24. A. Avellone, M. Benini, U. Moscato, Tactics for Translation of Tableau in Natural Deduction, TABLEAUX 99 (1999) (pdf)
      25. A. Avellone, M. Benini, D. Nowotka, Constructive Methods in Automatic Analysis of Correctness Proofs, LOPSTR 99 (1999).(pdf)
      26. M. Benini, D. Nowotka, C. Pulley, Computer Arithmetic: Logic, Calculation and Rewriting, FROCOS 98 (1998). Also available as a chapter in D. M. Gabbay, M. De Rijke eds., Frontiers of Combining Systems 2, Studies in Logic and Computation, Research Studies Press, 2nd edition (2000)  (pdf)
      27. M. Benini, S. Kalvala, D. Nowotka, Program Abstraction in a Higher Order Logic Framework, TPHOL 98 (1998). Also available in J. Grundy, M. Newey, Theorem Proving in Higher Order Logics: 11th International Conference, TPHOLs’98, Canberra, Australia, September 27 – October 1, 1998, Proceedings, Lecture Notes in Computer Science, Springer-Verlag, pp. 33-48 (1998) (pdf)
      28. M. Benini, Barendregt’s Lambda Cube in Isabelle, IUG (1995) (pdf)

Reviews

    1. M. Benini: review of Michal R. Przybylek, Logical systems. I: Internal calculi,  Journal of Pure and Applied Algebra 221, No. 2, 449-489 (2017), in ZentralBlatt MATH (2017) to appear
    2. M. Benini: review of R. Gangle, Diagrammatic immanence. Category theory and philosophy,  Edinburgh University Press (2016), in ZentralBlatt MATH (2017)
    3. M. Benini: review of F. Kachapova, A strong multi-typed intuitionistic theory of functionals, Journal of Symbolic Logic 80, No. 3, 1035-1065 (2015), in ZentralBlatt MATH (2017)
    4. M. Benini: review of R. Iemhoff, P. Rozière, Unification in intermediate logics, Journal of Symbolic Logic 80, No. 3, 713-729 (2015), in ZentralBlatt MATH (2017)
    5. M. Benini: review of F. Pasquali, Remarks on the tripos to topos construction: comprehension, extensionality, quotients and functional-completeness, Applied Categorical Structures 24, No. 2, 105-119 (2016), in ZentralBlatt MATH (2016)
    6. M. Benini: review of O. Caramello, Priestley-type dualities for partially ordered structures, Annals of Pure and Applied Logic 167, No. 9, 820-849 (2016), in ZentralBlatt MATH (2016)
    7. M. Benini: review of A.V. Zhozhikashvili, Monads for the formalization of a pattern matching procedure, Programming and Computer Software 40, No. 3, 117-127 (2014), in ZentralBlatt MATH (2015)
    8. M. Benini: review of B. Zieliński, P. Maślanka, S. Sobieski, Modalities for an allegorical conceptual data model, Axioms 3, No. 2, 260-279 (2014), in ZentralBlatt MATH (2015)
    9. M. Benini: review of A.A. Vladimirov, On a continuity theorem for constructive functions, J. Math. Sci., New York 199, No. 1, 6-15 (2014), in ZentralBlatt MATH (2015)
    10. M. Benini: review of D.I. Spivak, Category theory for the sciences, MIT Press (2014), in ZentralBlatt MATH (2015)
    11. M. Benini: review of the Univalent Foundations Program, Institute of Advanced Studies, Homotopy type theory: Univalent foundations of mathematics, Lulu Press (2013), in ZentralBlatt MATH (2014)
    12. M. Benini: review of P. Johnstone, What do Freyd’s toposes classify?, Logica Universalis, 7(3), pp. 335-340 (2013), in ZentralBlatt MATH (2014)
    13. M. Benini: review of S. Lee, J. van Oosten, Basic subtoposes of the effective topos, Annals of Pure and Applied Logic, 164(9), pp. 866-883 (2013), in ZentralBlatt MATH (2014)
    14. M. Benini: review of A. Rodin, Axiomatic method and category theory, Synthese Library 364, Springer (2014), in ZentralBlatt MATH (2014)
    15. M. Benini: review of C. McCarty, Paradox and potential infinity, in Journal of Philosophical Logic 42(1), pp. 195-219 (2013), in ZentralBlatt MATH (2013)
    16. M. Benini: review of F. Ciraulo, M.E. Maietti, P. Toto, Constructive version of Boolean algebra, in Logical Journal of the IGPL 21(1), pp. 44-62 (2013), in ZentralBlatt MATH (2013)
    17. M. Benini: review of G. Curi, Topological inductive definitions, in Annals of Pure and Applied Logic, 163, pp. 1471-1483 (2012), in ZentralBlatt MATH (2013)
    18. M. Benini: review of C. McLarty, Foundations as truths which organize mathematics, in The Review of Symbolic Logic, 6(1), pp. 76-86 (2013), in ZentralBlatt MATH (2013)
    19. M. Benini: review of P.T. Johnstone, Calibrated toposes, in Bulletin of the Belgian Mathematical Society 19, pp. 889-907 (2012), in  ZentralBlatt MATH (2013)
    20. M. Benini: review of M. Bezem, K. Nakata, T. Uustalu, On streams that are finitely red, Logical Methods in Computer Science, 8, 4(4), pp. 1-20 (2012), in ZentralBlatt MATH (2013)
    21. M. Benini: review of D. Skvortsov, Kripke sheaf completeness of some superintuitionistic predicate logics with a weakened constant domains principle, Studia Logica, 100(1-2), pp. 361-383 (2012), in  ZentralBlatt MATH (2013)
    22. M. Benini: review of E. Palmgren, Constructivist and structuralist foundations: Bishop’s and Lawvere’s theories of sets, Annals of Pure and Applied Logic, 163 (10), pp. 1384-1399 (2012), in ZentralBlatt MATH (2013)
    23. M. Benini: review of M.E. Maietti, S. Vickers, An induction principle for consequence in arithmetic universes, Journal of Pure and Applied Algebra, 216, pp. 2049-2067 (2012), in ZentralBlatt MATH (2012)

Dissertations

      1. M. Benini, Verification and Analysis of Programs in a Constructive Environment, Dottorato di Ricerca (PhD) (1999) (pdf)
      2. M. Benini, Circolarità, Minor Dottorato di Ricerca (1997) (pdf)
      3. M. Benini, Un approccio alla dimostrazione semiautomatica di teoremi mediante un calcolo logico basato sull’equivalenza, Laurea (1993)

Talks

    1. M. Benini, R. Bonacina, The Graph Minor Theorem: a walk on the wild side of graphs, JAIST Logic Seminar (2017)
    2. M. Benini, R. Bonacina, Explaining the Kruskal’s Tree Theorem, JAIST Logic Seminar (2017)
    3. M. Benini, R. Bonacina, The Graph Minor Theorem: a walk on the wild side of graphs, invited seminar in the Department of Computer Science, University of Verona (2017)
    4. M. Benini, Dealing with negative results, invited lecture in the course Research methods and proposal writing, held by Dr. Luca Longo, Dublin Institute of Technology (2016)
    5. M. Benini, Variations on the Higman’s Lemma, JAIST Logic Seminar series, Japan Advanced Institute of Science and Technology (2016)
    6. M. Benini, Dealing with negative results, invited lecture in the course Research methods and proposal writing, held by Dr. Luca Longo, Dublin Institute of Technology (2016)
    7. M. Benini, Well Quasi Orders in a Categorical SettingWell-quasiorderings: From Theory to Applications symposium at Jahrestagung der Deutschen Mathematiker-Vereinigung, Invited talk (2015)
    8. M. Benini, Proof-Theoretic Semantics: Point-free meaning of first-order systems, Trends in Proof Theory workshop at Jahrestagung der Deutschen Mathematiker-Vereinigung, Invited talk (2015)
    9. M. Benini, Point-free foundation of Mathematics, Logic seminar at the Yonsei University, Seoul, Republic of Korea (2015)
    10. M. Benini, Numerical Analysis and Epistemology of Information, workshop Philosophical Aspects of Computer Science, European Centre for Living Technology, University “Ca’ Foscari”, Venice, Invited talk (2015)
    11. M. Benini, Constructive Adpositional Grammars, Formally, DIP Colloquium, Institute of Logic, Language and Computation, University of Amsterdam, Invited talk (2015)
    12. M. Benini, Programming modulo representations, Algebra, Logic and Computation seminar at the University of Leeds, Invited talk (2014)
    13. M. Benini, F. Gobbo, Algorithms and their explanations, CiE 2014, special session History and Philosophy of Computing, Invited talk (2014)
    14. M. Benini, Programming modulo representations, Seminar at Logic group, School of Information Science, JAIST (2014)
    15. M. Benini, Point-free foundation of Mathematics, Seminar at Logic group, School of Information Science, JAIST (2014)
    16. M. Benini, Does programming really need data structures?, CORCON 2014, Correcteness by Construction, Keynote speech (2014)
    17. M. Benini, Fondazione point-free della matematica: una introduzione al ragionamento senza punti, Seminario di Logica, Dipartimento di Filosofia, Università degli Studi di Firenze, Invited talk (2013)
    18. M. Benini, Measuring Computational Complexity: the Qualitative and Quantitative Intertwining of Algorithm Comparison, Fifth Workshop on the Philosophy of Information (2013)
    19. M. Benini, Intuitionistic First-Order Logic: Categorical semantics via the Curry-Howard isomorphism, Logic Seminar, School of Mathematics, University of Leeds (2012)
    20. M. Benini, Adgrams: Categories and Linguistics, Proof Theory and Constructive Mathematics Seminar, School of Mathematics, University of Leeds (2011)
    21. M. Benini, Formal Connected Basic Pairs, Advances in Constructive Topology and Logical Foundations (2008) (pdf)
    22. M. Benini, G.A. Lanzarone, A. Spiriti, Navigazione tematica di un museo virtuale: una soluzione mirata, GARR Network Humanitatis (2007) (pdf)
    23. M. Benini, F. De Cindio, L. Sonnante, VIRTUOSE: An open-source Virtual Community Server, IIIrd Global Congress on Community Networking in the Digital Era (2002) (pdf)
    24. M. Benini, F. De Cindio, L. Sonnante, VIRTUOSE: a VIRTual CommUnity Open Source Engine, DIAC (2002) (pdf)
    25. M. Benini, The Collection Method in a Second Order Perspective, Intl. Conf. in Memoriam Pierangelo Miglioli (2000) (pdf)
    26. M. Benini, The Collection Method in Second Order Intuitionistic Logic, Logic Colloquium 98 (1998) (pdf)
    27. M. Benini, S. Kalvala, D. Nowotka, C. Pulley, HOLLY: An Approach to Object Code Verification, Intl. Workshop British Council on Theoretical Computer Science (1998)
    28. M. Benini, Sicurezza ed Internet: come affrontare il problema su Linux, parte II, I2U (1996)
    29. M. Benini, Sicurezza ed Internet: come affrontare il problema su Linux, I2U (1995)

Technical Reports

      1. M. Benini, A simplified definition of logically distributive categories, arXiv.org (2014)
      2. M. Benini, Cartesian closed categories are distributive, arXiv.org (2014)
      3. M. Benini, Intuitionistic First-Order Logic: Categorical Semantics via the Curry-Howard Isomorphism, arXiv.org (2013)
      4. M. Benini, Applications of Constructive Logics in Analysis, Verification and Synthesis of Programs, Notes for a PhD course in the Mathematische Institute of the Ludwig-Maximilian Universitaet, Muenchen, Germany (2006)
      5. M. Benini, Validating Object Code: strcmp, Dip. Sc. Inf. Tech. Rep. 249-00 (2000)
      6. A. Avellone, M. Benini, U. Moscato, Translating Tableaux into Natural Deduction: Applications to Theorem Proving, Dip. Sc. Inf. Tech. Rep. 240-99 (1999)
      7. M. Benini, The Collection Method in Second-Order Intuitionistic Logic, Dip. Sc. Inf. Tech. Rep. 237-99 (1999)
      8. M. Benini, Formal Verification of Hardware using HOL, Note del Polo 11, Crema (1998)
      9. M. Benini, Formal Verification of Hardware Circuits using HOL, Tech. Rep. SGS-Thomson (1996)
      10. M. Benini, M. Vaccari, Una dimostrazione di correttezza per il circuito SCRAMBLER nella versione parallela, Dip. Sc. Inf. Tech. Rep. (1994)
      11. M. Vaccari, M. Benini, G. Breviario, M. Bruschi, Computer Aided Logical Deduction: Specification of the SDL Language and Notes for its Implementation, Dip. Sc. Inf. Tech. Rep. (1993)
      12. M. Benini, G. Breviario, M. Bruschi, M. Vaccari, A Language for the Description and Implementation of Automated Theorem Provers, Dip. Sc. Inf. Tech. Rep. (1993)

Software

      1. M. Benini, prftree: a LaTeX package to write natural deduction proofs (v1.5 2016)
      2. M. Benini, F. Gobbo, adtrees: a LaTeX package to write adpositional trees, as used in Constructive Adpositional Grammars (v1.0 2016)

Non-research

      1. M. Benini, Un miracolo matematico, Tom’s Hardware (12 December 2016)

Non-scientific

      1. M. Benini (editor), M. Benini, F. Bertone, V. Del Bianco, C. Gentile, F. Gobbo, M. Ponzi, T. Torti, M. Vaccari (authors), Eroi che lanciano dadi, Lulu.com (2016)
      2. M. Benini, Portraits of Japan, Lulu.com (2015)

Disclaimer: all the pdf files of published material are preprints that differ from the printed papers. The pdf files are available for personal use only. In particular, the freely available pdf files may contain errors and no responsibility is taken on their content.