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