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

Craig McLaughlin Craig.McLaughlin at ed.ac.uk
Thu Apr 26 20:44:40 CEST 2018


Hi all,

I am trying to marry the description of the Iris base logic in the appendix:

https://plv.mpi-sws.org/iris/appendix-3.1.pdf

with the Coq formalisation.

In particular, I would like to know where the grammar of Section 5.1 is 
decorated with the typing judgment of Section 5.2. It seems like at 
least some of the iProp rules are defined in 
theories/base_logic/primitive.v but I cannot find the non-propositional 
rules.

-- 
Regards,
Craig
http://homepages.inf.ed.ac.uk/s1544843


The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.




More information about the Iris-Club mailing list