? ?
Notes from a Medium-Sized Island [entries|archive|friends|userinfo]

[ website | My Website ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

[Oct. 20th, 2003|07:22 pm]
Had some dinner, feeling a bit low again, but I see another angle on this stubborn, stubborn soundness proof. I am actually quite amused at how much this work has felt like programming, in that I am spending much of my time thinking about how to make good modules and good module boundaries, wondering what to abstract away, and what to expose.

I need to kick this habit of thinking that when people don't respond immediately to email, it means I have inscrutably and mysteriously done something to horribly offend them and they hate me forever and ever, and never wish to speak to me ever again &c. Unless this is actually the case. Doesn't seem too likely, but I like to cover all the bases.

[User Picture]From: easwaran
2003-10-21 02:23 am (UTC)
No, e-mail just often takes a while to respond to.

Good luck with the soundness proof.

Is what you're doing anything like what r6 does? I don't know if you've seen his lj yet. He's working on some sort of automation of a proof of Godel's Incompleteness Theorems. I think soundness was one of his earlier steps. Or are you proving soundness of some program, rather than a formal system?
(Reply) (Thread)
[User Picture]From: jcreed
2003-10-21 06:50 am (UTC)
Hey, neat! Thanks for pointing that out; I've been meaning to learn Coq for some time now, and I think his proof will be a good example to look at.

What I'm doing is trying to design a variant of the logical framework Twelf (a beast of the same general sort as Coq, the logical framework that r6 coded up his proof in) or, more to the point, a variant of its underlying type theory.

This variant is intended to be capable of omitting redundant information deep in the guts of proof objects, (saving memory, disk space, time, etc.) and uses a certain algorithm to reconstruct omitted information on the fly when it's needed. So I have shown completeness, that whenever something is well-typed (i.e. is a correct proof object within the systm) the algorithm says it is. Soundness --- that whenever the algorithm okays something, it really is okay in the original type theory --- is being a pain in the ass. But I think I'll get it eventually.
(Reply) (Parent) (Thread)
From: ctsm
2003-10-22 07:31 am (UTC)
i always think people hate me if they take more than a minute to im me. i win on the crazy scale!
(Reply) (Thread)