Alex Mobius (Apr 29 2026 at 20:57): Alex Mobius (Apr 29 2026 at 20:57):Working my way through domain theory, looking at its implementation in HOLCF. Powerdomains there have a general construction via ideal completion, but lack any sort of representation as sets of elements of base domains. Since HOLCF domains are super nice (omega-continuous bifinite), there should be nice representations of powerdomain elements as sets with specific properties. (That would also allow pairwise intersections). Is that missing from HOLCF? Maybe someone on AFP has implemented it? How are you meant to use powerdomains otherwise?
Kevin Kappelmann (Apr 30 2026 at 07:34):I don't know, but maybe the papers "HOLCF'11: A definitional domain theory for verifying functional programs" and "Reasoning with powerdomains in Isabelle/HOLCF" by Brian Huffman give details why things are the way they are
Alex Mobius (Apr 30 2026 at 10:01):@Kevin Kappelmann I can find a bunch of citations for the second paper, but no DOI or any reference to the source text at all, could oyu provide a pointer please?
Kevin Kappelmann (Apr 30 2026 at 13:12):I can't find it either :sweat_smile:
Kevin Kappelmann (Apr 30 2026 at 14:06):I think I got it (using ChatGPT + archive.org): https://web.archive.org/web/20240503140451/https://users.encs.concordia.ca/~tphols08/TPHOLs2008/ET/45-56.pdf
Alex Mobius (Apr 30 2026 at 14:16):Ah that seems to just be the chapter from the first reference, published independently. Interestingly the book proves some theorems about powerdomains' corresponding sets, but even formalization for those is missing.
Last updated: May 17 2026 at 06:46 UTC