Up: Progress Report Previous: University of Udine

University of Utrecht

Bezem did research at CWI in the period March 98 -- March 99, leading to the publications "Formulas as Programs" (together with Apt), and "Extensionality of Simply Typed Logic Programs". The book on Term Rewriting Systems is in its final (editorial) stage. Hendriks continued the work on the interface between resolution theorem provers (e.g. Bliksem) and the proof construction program Coq based on type theory (supervised by Bezem). He visited INRIA Rocquencourt for collaborating with the Coq community. Hendriks is currently visiting Saarbruecken to collaborate with de Nivelle in connecting Nivelle's theorem prover Bliksem to Coq.

Relevant publications:

K.R. Apt and M.A. Bezem, "Formulas as Programs", in: The Logic Programming Paradigm, ed. K.R. Apt, V.W. Marek, M. Truszczynski, D.S. Warren, pp. 75-107, Springer.

M.A. Bezem, "Extensionality of Simply Typed Logic Programs", in: Proceedings ICLP99, ed. D. de Schreye (to appear Nov. 99).

Up: Progress Report Previous: University of Udine