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. (-->) :: Process context (Linear context a) -> (forall context1. Process context1 (Linear context1 a) -> Process context1 a -> b) -> b ($=) :: Process context (Linear context a) -> Process context a -> (forall context1. Process context1 (Linear context1 a) -> b) -> b (-\) :: (Process context (Linear context a), Process context a) -> (forall context1. Process context1 (Linear context1 a) -> b) -> b lmap :: -------------------------------------------------- (==>) :: -------------------------------------------------- sample = 0 ==> \count0 -> By Steven StewartGallus at 2011-12-03 21:03 | LtU Forum | previous forum topic | next forum topic | other blogs | 5996 reads
|
Browse archives
Active forum topics |
Recent comments
16 weeks 8 hours ago
16 weeks 12 hours ago
16 weeks 12 hours ago
38 weeks 1 day ago
42 weeks 3 days ago
44 weeks 20 hours ago
44 weeks 20 hours ago
46 weeks 5 days ago
51 weeks 3 days ago
51 weeks 3 days ago