Computer Laboratory

Nik Sultana
Email:   nik.sultana ("at" symbol)
Tel:   +44 (0)1223 763773
Fax:   +44 (0)1223 334678
Smail:   Computer Laboratory
15 JJ Thomson Avenue
Cambridge CB3 0FD

Research Interests

  • Mechanical theorem-proving
  • Type theory, lambda calculus
  • Program/proof transformations
  • Functional programming
I'm interested in improving the usefulness of computers for building mathematical proofs. At present I'm working to interface Isabelle with higher-order automated proof tools. I'm also interested in programming theory and practice.

Recent talks

  • 7th June, Work in progress: A prototype refactoring tool based on a mechanically-verified core (details), at the ARG
  • 1st March, Rough-and-ready proof reconstruction (details), at the ARG
  • 23rd November, First prototype of an Isabelle/HOL-to-LeoII interface (details), at the ARG


  • Denotational semantics
  • Specification and verification
  • Logic and Proof
  • Concepts in Programming Languages

Some past talks


Things I've helped with


•  GH Hardy's review of Principia Mathematica is worth a read
•  A section of a Searle computing wall at the Computer Lab: