See also the web page for papers

Recent Talks

Nonstandard Models of Fragments of Church's Type Theory (CAMELEON, April 2008 in Cambridge) The last part of the talk is about an approach to the consistency problem for Quine's NF.

Scunak Proofreads a Latex Proof (MKM, 2006)

Scunak Related Talks

Scunak Proofreads a Latex Proof (MKM, 2006)

Ordinals in Scunak (CIAO, April 2006)

HOL Related Talks

Slides for Semantics of HOL at ESSLLI 2006, slides pdf, slides 4 on 1 page pdf;

Talks Before 2005

Benchmarks for Higher-Order Automated Reasoning (ESHOL Workshop at LPAR, Jamaica, December 2005) pdf I extracted thousands of higher-order theorems from the Jutting Automath encoding of Landau's book. (More information is here.) The challenge for a higher-order prover is to prove them.

Encoding Hybrid Logic in Higher-Order Logic (Loria, Nancy, April 2005) pdf ps Modal and hybrid logic operators can be defined in higher-order logic. This leads to consideration of typed modal and hybrid logics.

Induction and Cut (CIAO 2005, Nottingham, April 2005) pdf ps Induction axioms (as well as many other axioms) in impredicative logics allow cut simulation.

Thesis Related Talks given in the Math Logic Seminar, Spring 2004

Set Comprehension in Church's Type Theory (Part I)

Abstract

Set Comprehension in Church's Type Theory (Part II)

Abstract