The Coq mailing list

["Moez A. AbdelGawad" <moez AT cs.rice.edu>]

Dear interested Coq clubbers!

Given the multiple emails I recieved expressing interest in seeing my Coq7 extended abstract that reports on my experience with building a far-from-complete formalization of domain theory in Coq, forwarded below is an email I earlier sent to Nate and to the list but that didn't go thru for the list due to the attached file, so I stripped it out. The email explains why the abstract isn't available online.

As expressed in the email, until I update the abstract and post the new version online I don't at all mind sending the original abstract privately, as an attachment to separate emails, to anyone who requests it.

-Moez

-------- Original message --------
From: "Moez A. AbdelGawad" <moez AT cs.rice.edu> 
Date: 06/01/2018  07:44  (GMT+02:00) 
To: Nathaniel Yazdani <nyazdani AT cs.washington.edu>,coq-club AT inria.fr 
Cc: "Benjamin C. Pierce" <bcpierce AT cis.upenn.edu> 
Subject: RE: [Coq-Club] Domain theory in Coq

Hi,

Sure I don't mind. The abstract is attached. (Not sure though if coq-club rules allow messages with attachments to go through).

In 2015, when I tried posting this abstract on arXiv, it got rejected by some arXiv admin simply due to its very small size (it's two pages, as is normal for extended abstracts. I hope that arXiv have since changed their rules. However, I was very busy since that time with other errands so I didn't try reposting it or posting it elsewhere.)

Given that the info in the abstract is now slightly a little outdated (but the main conclusions remain), and given the renewed interest in Coq formalizations of domain theory, I think I will be soon updating the abstract and I may also add to it some more content (like some of my actual Coq code, to make the document longer but also more interesting I hope) then I will try posting the new version to arXiv.  If all goes well, I will make sure to keep you and coq-clubers informed.

-Moez

-------- Original message --------
From: Nathaniel Yazdani <nyazdani AT cs.washington.edu>
Date: 06/01/2018 05:28 (GMT+02:00)
To: coq-club AT inria.fr
Cc: "Benjamin C. Pierce" <bcpierce AT cis.upenn.edu>
Subject: RE: [Coq-Club] Domain theory in Coq

Hi,

I'm not the original poster, but I would also be interested in that extended abstract, if you don't mind sharing it with me.

Nate

On Jan 5, 2018 7:12 PM, "Moez A. AbdelGawad" <moez AT cs.rice.edu> wrote:

It will be very nice indeed if there are complete formalizations of domain theory in Coq, in the sense that they at least cover the basics of domain theory (eg, as in http://arxiv.org/abs/1605.05858), but surprisingly my impression is that unfortunately there aren't but incomplete ones.

When I tried developing one, in 2009, I partially found out why. The simplest domain theory proofs tended to be too lengthy and tedious when formalized in Coq. I included more details about my experience on formalizing (finitary-based) domain theory in Coq in an extended abstract that was published in 2015 (in Coq7) but that is not available online. (I can send that extended abstract to you if interested.)

If you reach a conclusion different than mine though, please make sure you share it with us.

-Moez

-------- Original message --------
From: "Benjamin C. Pierce" <bcpierce AT cis.upenn.edu>
Date: 05/01/2018 23:08 (GMT+02:00)
To: coq-club AT inria.fr
Subject: [Coq-Club] Domain theory in Coq


I’m looking for a nice development of “textbook domain theory” in Coq, to supplement some lectures in a graduate course.  Google pointed me to ones by Rob Dawkins and Nick Benton, but I’m sure there must be lots of others.  Any particular recommendations?

Thanks!

    - Benjamin