[Iris-Club] Two Monoid Questions
jung at mpi-sws.org
Fri Aug 16 14:21:18 CEST 2019
Probably just useful, and I think we could get a decent generalization of auth
without a lot of SProp infrastructure. That infrastructure will be nice if we
want to have more fancy relations, but I think we can leave that to future work.
I might give this a try on the train to ICFP and see how it goes. ;)
On 16.08.19 00:23, Gregory Malecha wrote:
> Is SProp essential? Or just useful for this?
> On Thu, Aug 15, 2019, 4:40 PM Robbert Krebbers <mailinglists at robbertkrebbers.nl
> <mailto:mailinglists at robbertkrebbers.nl>> wrote:
> On 14/08/2019 12.49, Ralf Jung wrote:
> > The annoying part is generalizing this to step-indexing, where we will need a
> > notion of "step-indexed relations". It is clear what that means (A -> B -> nat
> > -> Prop, down-closed and non-expansive), but so far we managed to avoid
> > realizing this notion in Coq. I have long advocated for adding it, though.
> Although I initially believed it would not be useful to have this notion
> since we didn't have machinery for doing proofs in SProp---we do have
> such machinery now! We can instantiate MoSeL with SProp, although it's
> not really a separation logic, we can just define P ∗ Q := P ∧ Q and
> <pers> P := P. I think it's worth a short to do this and see how useful
> it is.
More information about the Iris-Club