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  5908 reads

Browse archives
Active forum topics

Recent comments
19 weeks 3 days ago
23 weeks 5 days ago
25 weeks 2 days ago
25 weeks 2 days ago
28 weeks 17 hours ago
32 weeks 5 days ago
32 weeks 5 days ago
33 weeks 1 day ago
33 weeks 1 day ago
35 weeks 6 days ago