Sidestreets explored by looking at the "Retro" proof assistant LCF

An off-hand mention of "retro proof assistants" in a facebook comment had me look at LCF. It's been quite some time since I've read any CS theory outside of the more pragmatic side of PLT and FP, and even longer since I've read up on any logic or mathematical foundations. There's a bit on LCF in "Proof, Language, and Interaction". But now I've got some amazon orders to look forward to.

I wish I had been at this talk by Paulson:

http://events.inf.ed.ac.uk/Milner2012/slides/Paulson/LCF+-without-transitions.pdf

I remember coming across Skolem's paradox some time ago, and not really understanding it. I think I just had a quick look at the Wiki page and shrugged, getting on with something else (probably work).

Skolem's paradox:
http://en.wikipedia.org/wiki/Skolem%27s_paradox

The single slide on Skolem's "Paradox" in Paulson's talk above explains it in a nutshell. Nice.

UPDATE: The videos from the Milner Symposium are online:
http://events.inf.ed.ac.uk/Milner2012/videos.html