User loginNavigation 
Lightweight Static Capabilitites (II)The slides for the talk discussed here are now available for download. Like all of Ken and Oleg's work, this stuff is both cool and important. Keep in mind that the talk is quite different from the paper. The safety claims were formalized and proved in Twelf: list example, array example. To follow the proofs you should read them alongside the presentation slides. I am told that the first file might change soon, to reflect a more general proof. Perhaps Ken or Oleg would like to comment on the experience of doing mechanized proofs, a subject the comes up regularly on LtU. LtU newcomers, who already managed to take in a little Haskell or ML, may want to spend a little time chewing on this, and ask questions if something remains unclear, since this work may eventually have practical importance, and can teach quite a few interesting techniques. By Ehud Lamm at 20060829 08:34  Semantics  Software Engineering  Type Theory  other blogs  7578 reads

Browse archivesActive forum topics
New forum topics

Recent comments
8 hours 35 min ago
8 hours 46 min ago
1 day 14 hours ago
6 days 21 hours ago
1 week 1 day ago
2 weeks 5 days ago
3 weeks 4 days ago
4 weeks 4 days ago
6 weeks 2 days ago
6 weeks 5 days ago