[Iris-Club] Constructivism: necessity or preference?
jeehoon.kang at sf.snu.ac.kr
Sun Aug 14 08:40:59 CEST 2016
Dear Iris Club,
I would like to ask a question which is not really directly related to the
end users of the logic.. :-)
I think one of the design principle behind the Iris logic is
- In the ICFP 2016 paper is said "Dockins et al. introduced multi-unit
separation algebras , which, unlike PCMs, only demand the existence of
a possibly different unit ua with ua · a = a for any element a. A crucial
difference between multi-unit separation algebras and RAs is that we
present the monoidal operation and core as a function, whereas they
represent these as relations." I think the reason the authors think
function and relation have a crucial difference is, they care
- In the Iris 2.0 documentation, a COFE is defined as a tuple of the form
(T, =_n, lim: chain(T) -> T). It is stronger than requiring just existence
of the limit; it actually requires a function that maps a chain to its
My question is: is this constructivism necessary in the development of the
Iris logic? Or is it a preference?
- A subquestion is: is the constructivism related to the freedom from
all the axioms in the development?
- A remark: it seems that constructivism is applied somewhere, and
isn't elsewhere. For example the (CMRA-extend) rule merely requires the
existence of the decomposition, and not the construction of the
Jeehoon Kang (Ph.D. student) <http://sf.snu.ac.kr/jeehoon.kang>
Software Foundations Laboratory <http://sf.snu.ac.kr>
Seoul National University <http://www.snu.ac.kr>
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Iris-Club