Teaching






Dissertation





Curriculum Vitae





Bibliography





HYBRID





Recent Papers





Recent Talks


Picture




Alberto Momigliano



I've received my Ph.D. in the Pure and Applied Logic Program from Carnegie Mellon University in 2000. My adviser was Frank Pfenning. I moved to Leicester and then to Edinburgh, where I worked as a research scientist on the MRG and Mobius project. I'm now an associate professor at DI, University of Milan, Italy.

Contact information are available here. Scroll down for a list of recent papers and talks. If you're really a fan, please consult my full bibliography (here dblp) and my CV.

News:

  • I'm the PC co-chair of PPDP24, to be held in Milan Sept 9-11, 2024
  • I'm on the PC of LFMTP24

Some Past Events

  • I was on the PC of Certified Programs and Proofs (CPP), CPP 2024.
  • I was one of the local organizer of Logic Colloquium 2023, Milan June 2023. Web page
  • I've given a PhD course on Interactive Theorem Proving here at DI: link.
  • I was on the PC of LOPSTR'22, 32st International Symposium on Logic-based Program Synthesis and Transformation.
  • I was on the PC of FSCD2022 (International Conference on Formal Structures for Computation and Deduction), Haifa (Israel), but I resigned due to the war in Gaza.
  • Video of our POPLMark paper presented at ICFP 2020 (here, minute 58:00).
  • I was on the PC of LOPSTR'21, LSFA 2020 and of LSFA. 2019.
  • The Special Issue on the 31th Italian Conference on Computational Logic (CILC 2016) appears in Fundamenta Informaticae, vol. 161 (2018), Fiorentini, Pettorossi and myself editors.
  • CPP 2018 - The 7th International Conference on Certified Programs and Proofs. I was on the PC. Check out Brigitte's invited talk on our joint work.
  • CILC 2016 Convegno Italiano di Logica Computazionale, 20-22 giugno 2016. I was one of the chairs. The proceedings are published as volume 1645 of CEUR
 

Drafts

Publications

  • Gabriele Cecilia and A.M. A Beluga Formalization of the Harmony Lemma in the pi-Calculus. Proceedings Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2024), Tallinn, Estonia, 8th July 2024, Electronic Proceedings in Theoretical Computer Science 404, pp. 1–17. (PDF). (DOI).

  • Dale Miller and A.M. Property-Based Testing by Elaborating Proof Outlines (38 pages), July 2023, revised June 2024. To appear in TPLP. (CoRR).

  • Marco Carbone, A.M. and a bunch of others. The Concurrent Calculi Formalisation Benchmark. April 2024. link (PDF). COORDINATION'24 (DOI)

  • A.M. and Martina Sassella. More Church-Rosser Proofs in Beluga. LSFA2023. Slides, repo. June 2023. Appears in EPTCS Vol. 402

  • Marco Mantovani and A.M. Towards substructural property-based testing. (PDF). LOPSTR'21, March 2022. (DOI)

  • Matteo Manighetti, Dale Miller and A.M. Two applications of logic programming to Coq. Post-Proceedings of TYPES'20. LIPICS Vol. 188, June 2021, (PDF). (DOI)

  • Matteo Cavada, Andrea Colò and A.M. MutantChick: type-preserving mutation analysis for Coq. CILC'20 (PDF), Sept. 2020. CEUR, vol. 2710.

  • A.M. Why Proof-Theory Matters in Specification-Based Testing. ICTCS'20, (PDF), July 2020. CEUR Workshop Proceedings Volume 2756.

  • Roberto Blanco, Dale Miller, and A.M. On the Proof Theory of Property-Based Testing of Coinductive Specifications, or: PBT to Infinity and beyond. (Extended abstract), (Slides). TYPES2020 and LFMTP2020, March/June 2020.

  • Andreas Abel, Guillam Allais, Aliya Hameer, A.M., Brigitte Pientka, Steven Schaefer and Kathrin Stark. POPLMark Reloaded: Mechanizing Proofs by Logical Relations.Journal of Functional Programming. Dec 2019. PDF (40 pages). Appendix (30 pages), (DOI ).

  • Giorgio Marabelli & A.M. Formalizing the meta-theory of program equivalences in Coq. Web Page. ICTCS'19 Sept. 2019, Vol 2504 of CEUR.

  • Roberto Blanco, Dale Miller, and A.M. Property-Based Testing via Proof Reconstruction (full paper) (PDF) PPDP2019 . Oct 2019. (DOI ).

  • A.M. and Mario Ornaghi. The Blame Game for Property-based Testing. CILC 2019. June 2019 (PDF). Slides.

  • A.M., Brigitte Pientka and David Thibodeau. A Case Study in Programming Coinductive Proofs in Beluga: Howe's Method. Math. Struct. in Comp. Science, Cambridge University Press, (2019), vol. 29, pp. 1309–1343. (PDF), (DOI).

  • Francesco Komauli & A.M. Property-testing of abstract machines: an experience report. PDF. CILC 2018, 22--39, Bolzano, 20-22 Sept. 2018.

  • Mauro Ferrari, Camillo Fiorentini and A.M. From Constructivism to Logic Programming: an Homage to Mario Ornaghi. Fundamenta Informaticae, 161 (2018) 1–7.

  • Mario Ornaghi, Camillo Fiorentini and A.M. LOGI: A didactic tool for a beginners' course in logic (system description). In ICTCS 2017 and CILC 2017.

  • Guglielmo Fachini and AM. Validating the Meta-Theory of Programming Languages. SEFM'17, June 2017. (PDF)

  • James Cheney and AM. alphaCheck: A mechanized metatheory model-checker. (PDF). Theory and Practice of Logic Programming, May 2017. (DOI)

    • Roberto Blanco, Dale Miller, and A.M. Property-Based Testing via Proof Reconstruction: Work-in-progress. Draft June 2017. Slides. Presented at LFMTP'17.

  • Amy Felty, A.M. and Brigitte Pientka. Benchmarks for Reasoning with with Syntax Trees Containing Binders and Contexts of Assumptions. (PDF). Math. Struct. Comp. Science, May 2017. (DOI)

  • James Cheney, AM, Matteo Pessina. Advances in Property-Based Testing for alphaProlog. (PDF). TAP, July 2016.

  • Amy Felty, AM, Brigitte Pientka. An Open Challenge Problem Repository for Systems Supporting Binders. (PDF). LFMTP 2015: 18-32, June 2015.

  • Alessandro Avellone, Camillo Fiorentini, AM: A Semantical Analysis of Focusing and Contraction in Intuitionistic Logic. 140:3-4(2015), pp. 247-262. (PDF). This is the journal version of "Focusing on Contraction".

  • Amy Felty, A.M. and Brigitte Pientka. The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations. Part 2: A Survey. J. Automated Reasoning, July 2015. (DOI). We suggest you read the local copy, as Springer's typesetting, notwithstanding our efforts, is mediocre, to say the least.

  • Alessandro Avellone, Camillo Fiorentini, Alberto Momigliano: Focusing on Contraction. CILC 2013: 65-81. 2013. (PDF).

  • A. Tiu and A.M. Cut Elimination for a Logic with Induction and Co-induction. Journal of Applied Logic, 10(4): 330-367 (2012). (PDF). This paper offers a Girard-like proof of cut elimination, differently from arXiv:0812.4727. This is the extended journal version of the eponymous TYPES 2003 paper.

  • A.M. A supposedly fun thing I may have to do again: a HOAS encoding of Howe's method. Proceedings of the seventh international workshop on Logical frameworks and meta-languages, theory and practice, Copenhagen, Denmark, p. 33-42, (2012). Web page.

  • A. Felty and A.M. Hybrid: A Definitional Two Level Approach to Reasoning with Higher-Order Abstract Syntax. Journal of Automated Reasoning, 48(1): 43-105 (2012). (DOI) (PDF).

  • Camillo Fiorentini, AM, Mario Ornaghi and Iman Poernomo.  A constructive approach to testing model transformations. (PDF) Laurence Tratt, Martin Gogolla (Eds.): Theory and Practice of Model Transformations, ICMT 2010, Malaga, Spain, June 28-July 2, 2010. LNCS 6142 Springer 2010,

  • A.M. and Mario Ornaghi. Proof-theoretic and Higher-order Extensions of Logic Programming. A. Dovier and E. Pontelli (Eds.): 25 Years of Logic Programming in Italy, LNCS 6125, pp. 254--270. Springer, Heidelberg (2010). (PDF). @ Springer. June 2010,

  • A. Felty and A.M. Reasoning with Hypothetical Judgments and Open Terms in Hybrid. PPDP 2009 . (PDF). (DOI) @ ACM Press

  • Camillo Fiorentini , Mario Ornaghi, A. Momigliano and F. Pagano. Applying ASP to UML Model Validation. LPNMR 2009 . (PDF) . (DOI) @ Springer.

  • Camillo Fiorentini , Mario Ornaghi and A. Momigliano. Towards a type discipline for Answer Set programming. S. Berardi, F. Damiani, and U. de Liguoro (Eds.): TYPES 2008, LNCS 5497, pp. 117--135, 2009 @ Springer-Verlag Berlin. (DOI).

  • A.M., A. Martin and A. Felty. Two-Level Hybrid: A System for Reasoning Using Higher-Order Abstract Syntax (PDF).  LFMTP'07, ENTCS, Volume 196, Pages 1-152 (22 Jan 2008), originally submitted on May 2007 .

  • Mauro Ferrari, Camillo Fiorentini , Mario Ornaghi and A. Momigliano. Snapshot generation in a constructive object-oriented modeling language. (PDF, DOI ). Post-proceedings of  LOPSTR 2007, LNCS 4915 @ Springer, January  2008.

  • D. Aspinall, L. Beringer, M. Hofmann, H-W. Loidl and  A. Momigliano. A Program Logic for Resources. Theoretical Computer Science, 389(3): 411--445, Dec 2007.

  • D. Aspinall, L. Beringer and  A. Momigliano. Optimisation Validation.  Proceedings of the 5th International Workshop on Compiler Optimization meets Compiler Verification (COCV 2006). ENTCS, Volume 176, Issue 3, 19 July 2007, Pages 37-59  (DOI).

  • Mauro Ferrari, Camillo Fiorentini , Mario Ornaghi and A. Momigliano. Snapshot generation in a constructive object-oriented modeling language. (PDF), Pre-proceedings of  LOPSTR 2007, August  2007. Extended version with proofs (PDF).

  • James Cheney and A.M. Mechanized metatheory model-checking (DOI).  PPDP'07, July 2007.

  • A. Momigliano and B. Pientka (editors): preliminary proceedings of LFMTP:  International Workshop on Logical Frameworks and Meta-Languages: theory and practice. August 2006. Now published as Volume 174, Issue 5, Pages 1-150 (2 June 2007) of ENTCS: (link).

  • Mario Ornaghi, Marco Benini, Mauro Ferrari, Camillo Fiorentini and Alberto Momigliano. A Constructive Modeling Language for Object Oriented Information Systems. ENTCS, Volume 153, Issue 1, Pages 1-92  (PDF) (2006).

  • The MRG group. Mobile Resource Guarantees. Evaluation Paper. (PDF).  Marko C. J. D. van Eekelen (Ed.). Revised Selected Papers from the Sixth Symposium on Trends in Functional Programming, TFP 2005, Tallinn, Estonia, 23-24 September 2005. Trends in Functional Programming 6 Intellect 2007.

  • D. Aspinall, L. Beringer and  A. Momigliano. Optimisation Validation. Informatics@Edinburgh Publications, EDI-INF-RR-0509. Dec. 2005/Feb. 2006.  Slides of the talk.

  • A. Momigliano & Randy Pollack (Eds): Proceedings of the 3rd ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding. Sept. 2005,  Tallinn, Estonia. ACM DL, (link).

  • The MRG group. Mobile Resource Guarantees. Evaluation Paper. (PDF). August 2005. Presented at TFP 2005, Sixth Symposium on Trends in Functional Programming.

  • Mario Ornaghi, Camillo Fiorentini and Alberto Momigliano. Snapshots Generation via Constructive Logic. Extended Abstract, informal proceedings of MoVeLog'05, July 2005.

  • A. Momigliano and L. Beringer. Certification of Resource Consumption: From Types to (Logic) Programming. (HTML). Newsletter of the Association for Logic Programming (ALP), Vol. 18 n. 2, May 2005.

  • Mario Ornaghi, Marco Benini, Mauro Ferrari, Camillo Fiorentini and Alberto Momigliano. A Constructive Modeling Language for Object Oriented Information Systems (PDF). Proceedings of CLASE 2005. 

  • Kung-Kiu Lau, Alberto Momigliano and Mario Ornaghi. Constructive Specifications for Compositional Units, (PDF).  In Etalle, Sandro (Ed.): Proceedings of the Logic Based Program Synthesis and Transformation 14th International Symposium LOPSTR 2004, Verona Italy, August 26-28, 2004, Revised Selected Papers. Series LNCS vol. 3573, pp.198--214 @ Springer-Verlag, May. 2005.

  • L. Beringer, M. Hofmann, A. Momigliano and O. Shkaravska. Automatic Certification of  Heap Consumption. (PDF)  January 2005. In Franz Baader and Andrei Voronkov (editors): Proceedings of the 11th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR2004), Montevideo, Uruguay, March 14-18th, 2005. Volume 3452 of Lecture Notes in Artificial Intelligence @ Springer-Verlag. Slides (PDF).

    2004. July 2004.

  • L. Beringer, M. Hofmann, A. Momigliano and O.Shkaravska. Towards Certificate Generation for Linear Heap Consumption. Proceedings of  LRPP 2004, April 2004. (PDF).

  • D. Aspinall, L. Beringer, M. Hofmann, H-W. Loidl and  A. Momigliano. A Program Logic for Resource Verification. In Konrad Slind, Annette Bunker, and Ganesh C.Gopalakrishnan (editors): Proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs2004), Park City, Utah, September 14-17, 2004. Volume 3223 of Lecture Notes in Computer Science @ Springer-Verlag, February 2004.

  • A. Momigliano and A. Tiu. Induction and Co-induction in Sequent Calculus.
    Types for Proofs and Programs International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers. Series: LNCS, Vol.  3085. Berardi, Coppo, and Damiani Eds.  409 p.  Online version available January 2004.

  • A. Momigliano & F. Pfenning. Higher-Order Pattern Complement and the Strict Lambda-Calculus, ACM Transactions on Computational Logic,  pages: 493 - 529, Vol. 4 Issue 4, Oct. 2003. (PDF).

  • Simon Ambler, Roy Crole and A. Momigliano. A Combinator and Presheaf Topos Model for Primitive Recursion over Higher Order Abstract Syntax. Collegium Logicum (Proceedings of the Kurt Godel Society) @ Springer-Verlag, 2003.  Computer Science Logic/8th Kurt Godel Colloquium, Vienna, August, 2003.  (PS).

  • A. Momigliano and Jeff Polakow. A Formalization of an Ordered Logical Framework in Hybrid with Applications to Continuation Machines, June 2003. MERLIN 2003 @ ACM Press. ACM Digital Library. Isabelle code.

  • Simon Ambler, Roy Crole and A. Momigliano. A Definitional Approach to Primitive Recursion over Higher Order Abstract Syntax. June 2003. MERLIN 2003 @ ACM Press. ACM Digital Library.

  • A. Momigliano and Simon Ambler. Multi-Level Meta-Reasoning with Higher Order Abstract Syntax. Foundations of Software Science and Computational Structures 6th International Conference, FOSSACS 2003, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings Series: LNCS, Vol.  2620  Gordon, Andrew(Ed.)  2003, 441p.  Online version available@ Web page.

  • A. Momigliano, Simon Ambler and Roy Crole. A Hybrid Encoding of Howe's Method for Establishing Congruence of Bisimilarity. LFM'02, Volume 70.2 of ENTCS (PDF), Code.

  • A. Momigliano, Simon Ambler and Roy Crole. Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction. In 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLs02), Hampton, VA, 20-23 August 2002 (PDF), LNCS @ Springer-Verlag.

  • Simon Ambler, Roy Crole and A. Momigliano (Guest Editors). MERLIN 2001: Proceedings of the Workshop on MEchanized Reasoning about Languages with variable bINding, Electronic Notes in Theoretical Computer Science, Volume 58, Issue 1, November 2001. Technical Report, Leicester University, 2001/26, June 2001

  • A. Momigliano, Simon Ambler and Roy Crole. A Comparison of Formalizations of the Meta-Theory of a Language with Variable Bindings in Isabelle, Technical Report 2001/07, TPHOLs 2001 Category B paper, PS.

  • A. Momigliano. Elimination of Negation in a Logical Framework. PhD Thesis, available here as Technical Report CMU-CS-00-175, School of Computer Science, Carnegie Mellon University 21-26, 2000.

  • A. Momigliano. Elimination of Negation in a Logical Framework. Peter Clote, Helmut Schwichtenberg (Eds.): Computer Science Logic, 14th Annual Conference of the EACSL, Fischbachau, Germany, August 21-26, 2000, Proceedings. Lecture Notes in Computer Science 1862 Springer 2000, ISBN 3-540-67895-6. (PDF) (Abstract). An unshortened example of the method is here. Here is the Twelf code for the same example. LNCS @ Springer-Verlag

  • A. Momigliano & F. Pfenning. The Relative Complement Problem for Higher-Order Patterns. International Conference on Logic Programming (ICLP'99), Las Cruces, New Mexico, November 1999 (Abstract), (PS) (PDF).

  • A. Momigliano & M. Ornaghi. Towards a Logic for Reasoning about Logic Program Transformation. (PDF). Logic Program Synthesis and Transformation: 7th International Workshop, LOPSTR'97, Leuven, Belgium, July 1997. N.E. Fuchs (Ed.): pages 226-244. Lecture Notes in Computer Science, Springer-Verlag, ISSN: 0302-9743. Volume 1463 / 1998.

  • A. Momigliano & M. Ornaghi. Regular Search Spaces and Constructive Negation. Journal of Logic and Computation, v. 7, n. 3, pages 367-403, 1997. (PDF) (link).

    • For older papers, please consult DBLP.

Some Talks

  • An overview of PBT for the working semanticist. (Slides) Invited talk at King's College London and University of Sussex, June 2018

  • Property-Based Testing PL Artifacts: An experience report. CLA'17. Abstract. Slides.

  • Benchmarks for mechanized meta-theory: A very personal and partial view. Dagstuhl seminar on Universality of proofs, Oct 2016. Slides (pdf).

  • Toward a Theory of Contexts of Assumptions in Logical Frameworks. Theory and Application of Formal Proof , Laboratoire d'Informatique de l'Ecole Polytechnique, Novembre 2013. Slides (pdf).

  • Run your Research, Mind the Binders. McGill University, Agosto 2013. Slides (pdf).

  • On Howe's Method in Abella. Workshop on Abella, Bedwyr, and related systems, Laboratoire d'Informatique de l'Ecole Polytechnique, Luglio 2012. Slides (pdf).

  • A Supposedly Fun Thing I'll Have to Do Again. Certificates and Computation, Marzo 2012, ITU, Copenhagen. Slides (pdf).

  • A Practical Approach to Coinduction in Twelf. TYPES 2006, Nottingham, April 18-21, 2006. Slides (pdf).

For older talks, look here.