[Iris-Club] Two Monoid Questions

[Gregory Malecha]

Ah, that makes more sense. When you said SProp, I thought you meant the new
sprop Coq feature, not step-indexed propositions.

On Fri, Aug 16, 2019 at 9:58 AM Robbert Krebbers <
mailinglists at robbertkrebbers.nl> wrote:

> 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:
>
>    https://gitlab.mpi-sws.org/iris/iris/merge_requests/304/diffs
>
> 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
> >
>


-- 
gregory malecha
gregory at bedrocksystems.com
director of formal methods
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mpi-sws.org/pipermail/iris-club/attachments/20190816/727f5526/attachment.html>