headers
Karl Crary | 2 Jul 2008 21:10
Picon
Favicon

[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
Victoria, British Columbia, Canada
Sponsored by ACM SIGPLAN

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
(Continue reading)

Permalink | Reply | 0 comments |
headers
Brian Huffman | 23 Jul 2008 01:04
Picon

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
Permalink | Reply | 0 comments |
headers
Brian Huffman | 25 Jul 2008 03:23
Picon

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
(Continue reading)

Permalink | Reply | 0 comments |

Gmane