
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
MetaLanguages: 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 MetaLanguages: 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
ProofTheory of Logic Programming
Recent Drafts and
Publications
A.
Tiu and A.M. Cut Elimination for a Logic with Induction and
Coinduction. Journal of Applied Logic, 10(4):
330367 (2012). (PDF). This paper
offers a Girardlike 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 metalanguages, theory and
practice, Copenhagen, Denmark, p. 3342, (2012). Web
page.
A. Felty
and A.M. Hybrid: A Definitional Two Level Approach to
Reasoning with HigherOrder Abstract Syntax. Journal of Automated
Reasoning, 48(1):
43105 (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 28July 2, 2010. LNCS
6142 Springer 2010,
A.M. and Mario Ornaghi.
Prooftheoretic and Higherorder Extensions of Logic Programming.
A. Dovier and E. Pontelli (Eds.): 25 Years of Logic Programming
in Italy, LNCS 6125, pp. 254270. 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. 117135, 2009 @
SpringerVerlag Berlin. (DOI).
A.M., A. Martin
and A. Felty.
TwoLevel Hybrid: A System for Reasoning Using HigherOrder
Abstract Syntax (PDF).
LFMTP'07,
ENTCS, Volume 196, Pages 1152 (22 Jan 2008), originally
submitted on May 2007 .
Mauro
Ferrari, Camillo
Fiorentini , Mario
Ornaghi and A. Momigliano. Snapshot generation in a
constructive objectoriented modeling language. (PDF,
DOI ).
Postproceedings of LOPSTR
2007, LNCS 4915 @ Springer, January 2008.
D.
Aspinall, L.
Beringer, M.
Hofmann, HW.
Loidl and A. Momigliano.
A Program Logic for Resources. Theoretical Computer Science,
389(3): 411445, 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 3759 (DOI).
Mauro
Ferrari, Camillo
Fiorentini , Mario
Ornaghi and A. Momigliano. Snapshot generation in a
constructive objectoriented modeling language. (PDF),
Preproceedings of LOPSTR
2007, August 2007. Extended version with proofs (PDF).
James
Cheney and A.M. Mechanized metatheory modelchecking (DOI).
PPDP'07, July 2007.
A. Momigliano and B. Pientka
(editors): preliminary proceedings of LFMTP:
International Workshop on Logical Frameworks and MetaLanguages:
theory and practice. August 2006. Now published as Volume 174,
Issue 5, Pages 1150 (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 192 (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, 2324 September 2005. Trends in
Functional Programming 6 Intellect 2007.
D.
Aspinall, L.
Beringer and A. Momigliano. Optimisation
Validation. Informatics@Edinburgh Publications,
EDIINFRR0509. 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.
KungKiu
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 2628, 2004, Revised Selected
Papers. Series LNCS vol. 3573, pp.198214 @ SpringerVerlag,
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 1418th, 2005. Volume
3452 of Lecture Notes in Artificial Intelligence @
SpringerVerlag. Slides (PDF).
Longer version (PDF).
KungKiu
Lau, Alberto Momigliano and Mario Ornaghi.
Constructive Specifications for Compositional Units. (PS).
Preproceedings 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, HW.
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 1417, 2004.
Volume
3223 of Lecture Notes in Computer Science @ SpringerVerlag,
February 2004.
A. Momigliano and A.
Tiu. Induction
and Coinduction 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. HigherOrder
Pattern Complement and the Strict LambdaCalculus, 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) @
SpringerVerlag, 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. MultiLevel MetaReasoning with
Higher Order Abstract Syntax. Foundations of Software Science and
Computational Structures 6th International Conference, FOSSACS
2003, ETAPS 2003, Warsaw, Poland, April 711, 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,
2023 August 2002 (PDF),
LNCS @ SpringerVerlag.
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 MetaTheory 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 CMUCS00175, School of Computer Science,
Carnegie Mellon University 2126, 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 2126, 2000, Proceedings. Lecture
Notes in Computer Science 1862 Springer 2000, ISBN
3540678956. (PDF)
(Abstract).
An unshortened example of the method is here.
Here
is the Twelf code for the same example. LNCS @ SpringerVerlag
A. Momigliano & F.
Pfenning. The Relative Complement Problem for HigherOrder
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 226244. Lecture Notes in Computer Science,
SpringerVerlag, ISSN: 03029743. Volume
1463 / 1998.
A. Momigliano & M. Ornaghi.
Regular Search Spaces and Constructive Negation. Journal of Logic
and Computation, v. 7, n. 3, pages 367403, 1997. (PDF)
(link).
Some Talks
A Practical Approach to
Coinduction in Twelf. TYPES 2006, Nottingham, April 1821, 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. CometeParsifal 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 CoInduction in
Sequent Calculus. TYPES, Torino, May 1st 2003. (PS,
30 minutes talk), HeriotWatt, May 23rd (PDF,
60 minutes talk).
MultiLevel MetaReasoning 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 MultiLevel Reasoning
in Hybrid. LFM'02 ,
Copenhagen, July 26th 2002. Slides (PS).
A Definitional Approach to
HigherOrder 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 ProofSearch. April 2001,
Slides (PS).
Think Positive! Or Elimination of Negation in a Logical
Framework. Joint Theory Seminar, QMW, London, December 2000,
Slides (PS).
