** 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