User loginNavigation 
A question of separation logic and monadsI am slowly working my way up to an understanding of separation logic and one thing I have not seen with separation logic is a transformation into functional code with immutable data structures. With normal imperative code you just wrap a big fat monad around everything and there is a straightforward transformation into functional code with immutable data structures. The disadvantage of a big fat monad is that you loose the ability to reason about parts of the program that have side effects but are independent of each other. I would expect therefore that smaller monads that could be split and combined by the rules developed for separating logic and the separating conjunction would exist. Does anyone know if anyone has already research that? Or perhaps I am making an elementary error in my reasoning? By Eric Biederman at 20141004 21:38  LtU Forum  previous forum topic  next forum topic  other blogs  3469 reads

Browse archivesActive forum topics 
Recent comments
3 days 2 hours ago
1 week 6 days ago
2 weeks 6 days ago
3 weeks 1 day ago
3 weeks 1 day ago
3 weeks 1 day ago
4 weeks 5 days ago
4 weeks 6 days ago
5 weeks 2 hours ago
5 weeks 8 hours ago