Curriculum Vitae



Recent Papers

Recent Talks


Alberto Momigliano

Honorary Fellow in Computer Science

Laboratory for Foundations of Computer Science,
School of Informatics
The University of  Edinburgh
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 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

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).