User loginNavigation 
Proofs of a type system's safety?I was looking at linear types really hard lately. I made my own implementation of them in haskell. It's not a good implementation. I don't think it can handle multiple linear variables at once. As well, it's probable leakier than a sack full of holes. However, my code, attached below, isn't the topic I want to talk about anyways, rather I want to use it to raise another topic: how does one prove a type system has a desired property? What are some papers, proofs, tutorials and, books? Even just the right name to search for would be a good start. I have no clue how to prove that my system is actually safe. I don't even know what the actual theorem would look like in a formal notation. I don't even know what the formal notation would be! P.S. Please don't poke holes in my code. It's just a rough draft of the idea. Besides I'm asking about how people prove a type system works. Of course, I haven't taken a good look at my code. I don't know how to. P.S.S. Here's the attached code. The basic idea is there is a context variable in the type. Every time one reads or writes a variable one get's some new context variable and therefore one can't mix the past and the future or two concurrent events.
By Steven StewartGallus at 20111203 21:03  LtU Forum  previous forum topic  next forum topic  other blogs  4398 reads

Browse archivesActive forum topics 
Recent comments
1 day 7 hours ago
1 day 11 hours ago
2 days 11 hours ago
2 days 13 hours ago
2 days 19 hours ago
3 days 12 hours ago
3 days 21 hours ago
4 days 8 hours ago
4 days 9 hours ago
4 days 9 hours ago