|
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 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
Publications
Daniel Zackon, Chuta Sano, A.M. and Brigitte Pientka.
Split Decisions: Explicit Contexts for Substructural Languages. Nov 2024. To appear in CpP25.
(Artifact)
- 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.
|