| Teaching |
||
| Dissertation | ||
| Curriculum Vitae | ||
| Bibliography | ||
| HYBRID | ||
| Recent Papers | ||
| Recent Talks |
||
| Picture |
||
Alberto Momigliano
| Honorary Fellow in Computer Science Laboratory for Foundations of Computer Science, School of Informatics The University of Edinburgh, Edinburgh EH8 9AB, Scotland, UK. e-mail: amomigl1 at inf dot ed dot ac dot uk |
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 DSI,
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:
- 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)
Some Past Events
-
LFMTP 2010 at FLOC'10. Edinburgh, Scotland July 14, 2010
- 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.
- LFMTP 2009 4th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice. Affiliated with CADE-22, August 2-7, McGill University, Montreal, Canada: I was a PC member
- LFMTP'08:
International
Workshop on
Logical Frameworks and Meta-Languages: Theory and Practice. Affiliated
with LICS-23
at Pittsburgh, Pennsylvania, 23
June 2008 - I was in the
PC.
- ICTCS 2007 Tenth Italian Conference on Theoretical Computer Science. Rome, Italy, October 3--6, 2007 -- PC member.
- International Workshop on Logical Frameworks and Meta-Languages: theory and practice (LFMTP). A FLOC 2006 Workshop, August 16, 2006, Seattle, USA - I was the organizing chair and in the PC.
- Merlin 2005, Friday, 30 Sept. 2005, in association with ICFP 2005. I was the organizing chair and in the PC.
- ETAPS 2005. I was in the organizing committee as tutorial chair
- Special Issue of Higher-Order and Symbolic
Computation on
"MEchanized Reasoning about Languages with variable bINding", following
the Second ACM SIGPLAN Workshop MERLIN 2003 http://merlin.dimi.uniud.it.
Research Interests
- Logical Frameworks and (Co)Induction
- PCC, resources and the lot
- Formal Verification and Automated Reasoning
- Proof-Theory of Logic Programming
Recent Drafts and Publications
- A. Felty and A.M.
Hybrid: A Definitional Two Level Approach to Reasoning with
Higher-Order Abstract Syntax. Accepted for publication in the
Journal of Automated Reasoning , August 2010. (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. Tiu and A.M. Cut Elimination for a Logic with Induction and Co-induction. March 2010, revised Sept. 2010 (PDF). This paper offers a Girard-like proof of cut elimination, differently from arXiv:0812.4727.
- 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. Tiu and A.M. Induction and Co-induction in Sequent Calculus. Dec. 2008, arXiv:0812.4727 . This is the extended journal version of the eponymous TYPES 2003 paper.
- 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).