2 Jul 2008 21:10

### [TYPES/announce] WMM'08 call for papers (reminder)

```[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

A friendly reminder to all methatheory mechanizers: abstracts for WMM'08
are due tomorrow.

(Apologies for the cross posting.)
-----------------------------------------

Call for Papers

3rd Informal ACM SIGPLAN Workshop on Mechanizing Metatheory

Co-located with ICFP’08.
http://www.cis.upenn.edu/~sweirich/wmm/

Important Dates

* Submission deadline: 3 July 2008
* Author Notification: 1 August 2008
* Workshop: 20 September 2008

Workshop Description

Researchers in programming languages have long felt the need for tools
to help formalize and check their work. With advances in language
technology demanding deep understanding of ever larger and more complex
languages, this need has become urgent. There are a number of automated
```

23 Jul 2008 01:04

### ordering lemmas about powerdomain operations

```[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hello all,

I have been formalizing some properties of powerdomains and their
operations in the Isabelle theorem prover. For example, one of the
lemmas that I have proved is the following one about the upper
powerdomain:

xs + ys << {z} if and only if xs << {z} or ys << {z}

where (+) is the binary union operation, {-} is the monadic unit or
singleton, and (<<) is the information-ordering relation.

Someone must have proved some ordering lemmas like this previously,
but I haven't come across any in the papers I have looked at.
Descriptions of upper or lower powerdomains usually mention that they
are semilattices with the binary union acting as the meet or join;
being a semilattice entails a bunch of lemmas about (+) alone, but
doesn't say anything about properties of (+) combined with {-} as in
my example above.

Does anyone have a reference to a paper that proves (or even just
lists) any of these ordering lemmas for powerdomains?

- Brian Huffman

```
25 Jul 2008 03:23

### Re: ordering lemmas about powerdomain operations

```[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Quoting Thomas Streicher <streicher@...>:

> The lemma you mention is obvious from the way how the Smyth (i.e.
> upper) powerdomin
> is constructed, namely as nonempty compact upward closed subsets of
> the domain
> ordered by \supseteq. From this it is trivial.
> Moreover one has in the Smyth powerdomain  x \sqsubseteq y  if  x \cup y = x.
>
> Information about powerdomains can be found in the respective papers
>  by Plotkin
> and Smyth from the 70ies.
> You might want to have a look at
>
>     http://homepages.inf.ed.ac.uk/gdp/publications/Domains.ps
>
> for example.
>
> Thomas

I'm not sure that I am familiar with the construction of the upper
powerdomain that you describe, unless you are referring to the
construction of Smyth powerdomains over flat element types from the
linked paper. I failed to specify in my original question, but I am
interested in element types that are arbitrary omega-bifinite domains.

In my formalization I construct three varieties of powerdomains using
ideal completion, with a basis Pfin(K(a)) consisting of nonempty
```