tag:blogger.com,1999:blog-11162230.post2796105551750250447..comments2017-03-29T06:29:23.865-07:00Comments on Jeremy Siek: Type Safety in Three Easy LemmasJeremy Siekhttps://plus.google.com/115359947417709201623noreply@blogger.comBlogger4125tag:blogger.com,1999:blog-11162230.post-76486229683225638882013-07-19T06:06:12.473-07:002013-07-19T06:06:12.473-07:00Thanks, fixed!Thanks, fixed!Jeremy Siekhttp://www.blogger.com/profile/13773635290126992920noreply@blogger.comtag:blogger.com,1999:blog-11162230.post-12797745096319966242013-07-18T18:28:04.527-07:002013-07-18T18:28:04.527-07:00Just a quick typo: Turing-complete is misspelled a...Just a quick typo: Turing-complete is misspelled as Turning-complete.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-11162230.post-91020088259773840792013-07-01T13:39:28.981-07:002013-07-01T13:39:28.981-07:00Great! Thanks for sharing!
That would be interest...Great! Thanks for sharing!<br /><br />That would be interesting if you could find a constructive way to define eval. (Though I wouldn't hold my breadth.)<br /><br />I forget why I said typeof is partial... in my Isabelle version it is total. I've now linked to my Isabelle development at the beginning of the post.Jeremy Siekhttp://www.blogger.com/profile/13773635290126992920noreply@blogger.comtag:blogger.com,1999:blog-11162230.post-44924692063640193502013-06-29T01:24:31.841-07:002013-06-29T01:24:31.841-07:00I was curious to try how this proof would go throu...I was curious to try how this proof would go through in Coq, and the result was - surprisingly easy. (The current Coq source is here: https://gist.github.com/dkrustev/5890291) As I used Coq's functional induction (for the first time) for the 3rd lemma, it required considering 16 cases, not 6 (including cases when some intermediate computation times out or gets stuck), but most of these cases were easy to deal with. One thing I realized only during the Coq formalization - though, in retrospect, it should have been obvious from the beginning - was that while all lemmas have constructive proofs, the main theorem does not. It appears this non-constructiveness follows from the way \mathit{eval} is defined. I still wonder if another definition of \mathit{eval} would be possible, giving both fully constructive proofs and a similar level of simplicity ... Another minor point: the \mathit{typeof} function is actually total in the Coq formalization, but it probably depends on the exact encoding of the language syntax.Dimitur Krustevhttp://www.blogger.com/profile/01461994661311615344noreply@blogger.com