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