Konrad Slind

I am a member of ARG -- the Automated Reasoning Group -- at the Computer Laboratory in Cambridge University. My main area of interest is the implementation and application of logic, higher order logic especially. I have written a few papers in the area. Among my current and former projects are the following:

PROSPER

The PROSPER project aims at componentizing theorem proving tools so that they can be more widely used.

Hol98 is a Moscow ML-based implementation of the HOL logic, incorporating many features not found in other HOL systems. Hol98 technology appears in tools currently under development in the PROSPER project.

TFL

This refers to an environment (currently used by both HOL and Isabelle/HOL) for defining and reasoning about recursive, but total, 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. I'm interested in developing a deduction-based strong functional programming environment with it.

CLAM/HOL

This was an exercise in combining two large theorem proving systems. It was conducted in cooperation with Richard Boulton then at Edinburgh University, now at Glasgow.

---

[Family Pics]
[Rafting at CADE (raftmates John Harrison, Andrew Appel, and Bruce Spencer)] [Rafting] [Rafting]
[Schedule]

---

Postal Address:  Konrad Slind
                 University of Cambridge Computer Laboratory
                 New Museums Site
                 Pembroke Street
                 Cambridge CB2 3QG
                 United Kingdom
Phone:           +44 1223 334729  (Work)
                 +44 1954 210877  (Home)
Room:            TP1
email:           kxs@cl.cam.ac.uk

---