tag:blogger.com,1999:blog-11162230.post2796105551750250447..comments2022-12-10T01:04:18.836-08:00Comments on Jeremy Siek: Type Safety in Three Easy LemmasJeremy Siekhttp://www.blogger.com/profile/13773635290126992920noreply@blogger.comBlogger6125tag:blogger.com,1999:blog-11162230.post-46102322865056519972018-05-11T14:49:50.403-07:002018-05-11T14:49:50.403-07:00Yes, darn Dropbox change a while back regarding Pu...Yes, darn Dropbox change a while back regarding Public directory access. I've fixed the link. Thanks for pointing this out!Jeremy Siekhttps://www.blogger.com/profile/13773635290126992920noreply@blogger.comtag:blogger.com,1999:blog-11162230.post-70163404844906352522018-05-11T13:10:57.346-07:002018-05-11T13:10:57.346-07:00Hi Jeremy, awesome post thanks! The link to the Is...Hi Jeremy, awesome post thanks! The link to the Isabelle development is not working anymore. Is it still available somewhere? Thanks! Ranjit.<br />Anonymoushttps://www.blogger.com/profile/16831295285289260322noreply@blogger.comtag: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 Siekhttps://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 Siekhttps://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 Krustevhttps://www.blogger.com/profile/01461994661311615344noreply@blogger.com