Andres Erbsen

oh, I think you are right about `runExt`. I'll think more about this tomorrow.

I don't think we should squash together the "io" monad and the state monad. The compiler will need to spill variables when it runs out of registers, and this should...

none of the approaches I proposed work with the current fuel-based semantics. the program that takes n as input and then counts to n cannot be shown to terminate (for...

What you are saying makes sense, but I think the correct notion of "termination" for programs with io is that there is a finite number of steps between every pair...

It seems that deepspec people are also converging on a semantics similar to the coinductive monadic denotational style you propose. I am still keeping my eyes open about this, but...

That's just what he said, if I get a chance I'll ask for more information. I am guessing it is just the usual "oh Coq infrastructure doesn't really have support...

another related discussion at deepspec: ~~~~~ deepspec talk about setl4 concurrency verification first talk about the implementations, then theory, then proof sketch for verification single core sel4 recap: 1. 3k...

I think I have now talked to almost everybody at deepspec who has been working on interaction tree semantics, and I have gained relatively little additional insight. The overall picture...

It' not quite lists, but I refactored the explicit stacks code in https://github.com/mit-plv/bedrock2/compare/io-explicit-stacks based on Gregory's suggestions and it indeed looks more modular now. :+1: The proposal for using this...

@samuelgruetter I talked to Gregory about the diff I posted, and we think that we might stick with it for now. I will now go refactor the semantics some more...