[Iris-Club] Two Monoid Questions

Robbert Krebbers mailinglists at robbertkrebbers.nl
Fri Aug 16 15:58:13 CEST 2019

I realized I defined the type sProp in Coq a long time ago already, but 
never created a merge request for it. I have done that now:


I propose we continue this discussion there.

On 16/08/2019 14.30, Ralf Jung wrote:
>> By defining SProp, I suppose you would also define the logical operators and
>> prove that it's an step-indexed intuitionistic logic?
> No, I'd just define the notion of down-closed predicates, and show that they
> form a COFE.  I'd show that `dist` can be written as one (and maybe validity
> too, for fun's sake).  And that's about all I need to get started.
> Even independent of a proof mode instance this opens all sorts of questions:
> should `dist` be define as one of these? Should `UPred` use this? Should there
> be embeddings to/from the Iris Base Logic?
> For now, I am only interested in what is needed to generalize auth.
> ; Ralf

More information about the Iris-Club mailing list