James Smith

James Smith

james.smith@openmathematics.org (related to academia)
james.smith@djalbat.com (all other)

I am a mathematician and programmer, almost exclusively JavaScript these days. I have worked very briefly with temporal logics in the past, inventing a new one (this is nothing very clever, new logics are invented all the time) and proving that it is equivalent to some others. I also seem to have devised what appears to be the first correct concurrency control algorithm, at least going by one commonly held definition. These days I am working on a proof assistant called Occam, if that's not obvious.


Earlier this year I was kindly invited out to France to talk with others about formal mathematics. I ended up giving an impromptu talk and have just gotten around to completing the slides that would have gone with it. It is the first real mathematics I've done with Occam and so a subject that's close to my heart. And I'm claiming (with pantomime hubris, perhaps) that it's novel. Anyway, you can find the slides in the new presentations section below.

I should take this opportunity to sincerely thank Josef Urban and Henk Barendregt for their interest in Occam.

[show older]


Occam has its own dedicated page including a section on how you can get it running locally.



These are not fully peer-reviewed papers and should not be judged as such.




Last updated 16th September, 2018.