Konrad Slind's Research

I'm particularly interested in classical higher order logic, its implementation, and its application to the verification of system properties. I have been developing HOL4, a Moscow ML-based implementation of the HOL logic, with colleagues for a number of years. We have recently moved the development to SourceForge. Interested in being involved? Drop me a line.

Some places and projects I was involved with before coming to Utah:

PROSPER

The PROSPER project aimed at componentizing theorem proving tools so that they can be more widely used. It uses Hol98 technology internally. The European Commission profiles PROSPER in the May 2002 issue of its Technology Opportunities Today magazine.

ARG

I was a member of the Automated Reasoning Group at the Computer Laboratory in Cambridge University.

Isabelle at Munich

Before that, I was a member of the Isabelle group in Munich (where I obtained my PhD).

TFL

TFL is a package, currently used in both HOL and Isabelle/HOL, for defining and reasoning about total recursive functions in higher order logic. TFL supports the definition of recursive functions via ML-style pattern matching, as well as inductive proofs of properties of such functions.

CLAM/HOL

This was an exercise in combining two large theorem proving systems, conducted in cooperation with Richard Boulton (then at Edinburgh University, and until September 2001 at Glasgow).

---

Konrad Slind, slind@cs.utah.edu