[Iris-Club] Well-Typedness of the Base Logic

Danny Gratzer jozefg at cmu.edu
Thu Apr 26 21:16:21 CEST 2018


Hello,

I hope I am not misunderstanding your question but I believe the answer is
that this step is never done
explicitly.

The iris-coq formalization is a shallow embedding so there is no explicit
Coq datatype for the syntax of base logic terms.
Functions are represented as normal Coq functions so there is no need to
explicitly specify the typing rules governing
them: they're built into Coq. Similarly with products, sums, etc. Once the
type of propositions, iProp, is defined in Coq
Iris propositions are just represented as  normal Coq terms belong to iProp.

I think that there should then really be no analog of 5.2 explicitly, it's
encompassed in how the object terms
are represented in Coq in the first place.

This is why, for instance, the definition of weakest preconditions we are
able to take a guarded fixed point of
a normal Coq function (see wp_def in theories/program_logic/weakestpre.v).

Danny
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mpi-sws.org/pipermail/iris-club/attachments/20180426/3d552a61/attachment.html>


More information about the Iris-Club mailing list