Alberto Momigliano

I've received my Ph.D. in the Pure and Applied Logic Program from Carnegie Mellon University with a dissertation entitled "Elimination of Negation in a Logical Framework" in 2000. My adviser was Frank Pfenning. I then moved to Edinburgh in 2003, where I worked on the MRG and Mobius project.

I'm now an assistant professor at DI, University of Milan, Italy.

Contact information are available in my plan file. Here's a list of recent papers and talks. If you're really a fan, please consult my full bibliography (here dblp) and my CV.

Forthcoming Events:

• LFMTP13, International Workshop on Logical Frameworks and Meta-Languages: theory and practice. In association with ICFP2013, Boston MA September 24, 2013. I'm one of the organizers

Some Past Events

• ITP12, Interactive Thereom Proving, Princeton. I wasa PC member.

• LFMTP12, International Workshop on Logical Frameworks and Meta-Languages: theory and practice. Copenhagen.

• A graduate course at DSI: Linear Logic: Theory and Applications, given by Marco Gaboardi, Alberto Momigliano, and Carsten Schürmann. April 28–May 11, 2011. (Outline)

• A graduate course at DSI: Proof Search and Computation, by Dale Miller (link). On March 16, there was an informal workshop, here is the program.

Research Interests

• Logical Frameworks and (Co)Induction

• PCC, resources etc.

• Formal Verification and Automated Reasoning

• Proof-Theory of Logic Programming

Recent Drafts and Publications

• 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). Longer version (PDF).

• Kung-Kiu Lau, Alberto Momigliano and Mario Ornaghi. Constructive Specifications for Compositional Units. (PS). Pre-proceedings of LOPSTR 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).

Some Talks

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

• A Program Logic for Resources and its Application to Optimisation Validation. Udine, Nov 29th, QMUL, Dec 1st, 2005. Slides (pdf).

• Automatic Certification of Resource Consumption. Comete-Parsifal Seminar, Echole Polythecnique, Paris. March 7th, 2005. Slides (pdf).

• Towards Certification of Resource Consumption. Dreamers Seminar, November 5h 2004. Edinburgh. Slides (pdf).

• From Bytecode Logic to Certificate Generation for Grail, Global Computing Workshop, March 11th 2004, Rovereto. Slides (pdf).

• A Formalization of an Ordered Logical Framework in Hybrid, Merlin'03, Uppsala, August 26th 2003. Slides (pdf).

• Induction and Co-Induction in Sequent Calculus. TYPES, Torino, May 1st 2003. (PS, 30 minutes talk), Heriot-Watt, May 23rd (PDF, 60 minutes talk).

• Multi-Level Meta-Reasoning with Higher Order Abstract. FOSSACS,  Warsaw, April 8th 2003. Slides (PS).

• A Hybrid Logical Framework. INRIA Rocquencourt, January 31st 2003. Slides (PS).

• Simple Compiler Verification in a Hybrid Logical Framework. Nottingham Theory Seminar, December 6th 2002. Slides (PS).

• Towards Multi-Level Reasoning in Hybrid. LFM'02 , Copenhagen, July 26th 2002. Slides (PS).

• A Definitional Approach to Higher-Order Abstract Syntax. SPAM Seminar, Yale University, April 2002, Slides (PS).

• Algebraic Operations over First and Higher Order Terms. MCS Internal Seminar, November 2001, Slides (PS).

• A "Negative" Look to Uniform Proof Search. Dagstuhl Seminar on Semantic Foundations of Proof-Search. April 2001, Slides (PS).

• Think Positive! Or Elimination of Negation in a Logical Framework. Joint Theory Seminar, QMW, London, December 2000, Slides (PS).