I’m giving a talk in the Philosophy colloquium here at U. Iowa this afternoon, and I wanted to post a link to my slides, as well as links to some papers I reference:

- “Astree: From Research to Industry”, D. Delmas, J. Souyris, SAS 2007 (Springer).
- “seL4: Formal Verification of an OS Kernel”, G. Klein et al., SOSP 2009.
- “Formal Proof: The Four Color Theorem”, G. Gonthier, Notices of the AMS, 2005.
- “Weyl’s Predicative Classical Mathematics as a Logic-Enriched Type Theory“, R. Adams, Z. Luo, ACM TOCL, 2010.
- “Logical Frameworks — A Brief Introduction”, F. Pfenning, 2002.
- “Outline of a Theory of Truth”, Saul Kripke, Journal of Philosophy, 1975.

### Like this:

Like Loading...

*Related*

## 7 Comments

I just had a look of your nice slides. I like the idea of a coinductive treatment of self-reflective languages. Do you have any references to prior or current work on this? I know that theories for self-reflecting truth can be interpreted with fixed points, but in the usual account the semantics of the truth predicate is grounded in the atomic formulas.

Hi, Ulrik. I do not have any references to work on that idea. I suppose probably the right thing to look at would be some of the work of Barwise and Etchemendy, since (from what I read in other sources) they are concerned with similar problems, and may be using related technical solutions. So next on my list of things to look at will probably be “The Liar: an Essay in Truth and Circularity.”, by those two authors.

Do you have any other sources to recommend?

Hi, Aaron. Sorry for the late reply.

The only other source I’ll recommend, and which I’m sure you’re already familiar with, is Sol Feferman’s JSL paper “Reflecting on Incompleteness”. There, Kripke’s partial predicates are axiomatized and studied proof-theoretically.

Great talk!. It is still surprising to me how many fields are applicable to CS. I look forward to looking over your references.

Harley

Thanks, Harley!

I just read the Kripke paper you linked. It really is striking how similar this is to the standard denotational semantics for programming languages — and I guess it’s roughly contemporary with Scott’s work too?

So what did the philosophers think about all this?

Hi, Vilhelm.

Yes, I was really struck by the similarity, too, and got very excited about the paper. I thought it would be definitely one that would be of interest to the philosophy audience at the talk Friday.

Fortunately, before “introducing” it to them, I did a little searching around to see if others had picked up on that paper in the Philosophy literature. Boy have they ever! It is hands-down one of the top two most influential papers in the area in the 20th century (the other being a paper of Tarski that seems largely to have gotten the modern conversation of the liar paradox going). So they do know it very well, and there seems to have been a lot of work following from it.

Aaron