I 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 (and will be) 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:

  • Daniel has given a talk about "Mechanizing linear logical relations" at TLLA25.
  • Our CPP paper "Split Decisions" won the Distinguished paper award (link)
  • I'm on the PC of PPDP2025
  • I'm on the PC of LSFA2025
  • I'm on the Steering Committee of PPDP

Some Past Events

  • I was the PC co-chair of PPDP24, held in Milan Sept 9-11, 2024
  • I was on the PC of LFMTP24
  • 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

Marco Carbone and A.M. Mechanising the Meta-Theory of Session Types in Rocq: a Tutorial. (PDF) August 2025.

Publications

Daniel Zackon, Chuta Sano, A.M. and Brigitte Pientka. Split Decisions: Explicit Contexts for Substructural Languages. Nov 2024. CPP25. (Artifact) (DOI)

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. TPLP, Volume 24 Issue 6. (CoRR) (DOI)

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.

A.M., A. Martin and A. Felty. Two-Level Hybrid: A System for Reasoning Using Higher-Order Abstract Syntax. 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.

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