coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Domain theory in Coq

From: Nathaniel Yazdani <nyazdani AT cs.washington.edu>
To: coq-club AT inria.fr
Cc: "Benjamin C. Pierce" <bcpierce AT cis.upenn.edu>
Subject: RE: [Coq-Club] Domain theory in Coq
Date: Fri, 5 Jan 2018 19:28:29 -0800
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=nyazdani AT cs.washington.edu; spf=None smtp.mailfrom=nyazdani AT cs.washington.edu; spf=None smtp.helo=postmaster AT mail-qk0-f171.google.com
Ironport-phdr: 9a23:+xoZzhGTx5IfXXsOf2n7EZ1GYnF86YWxBRYc798ds5kLTJ7zpsWwAkXT6L1XgUPTWs2DsrQY07OQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmCexbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VC+85Kl3VhDnlCYHNyY48G7JjMxwkLlbqw+lqxBm3oLYfJ2ZOP94c6jAf90VWHBBU95TWCxPAo2yYYgBAfcfM+lEtITyvUcCoAGkCAWwGO/iyDlFjWL2060g1OQhFBnL0hQ6ENISsHTbttP1NKYMXuCx0aLHzy/MbvJL1jjn7ojIcw0qrPaKXbNwa8XQyFQgGBnDjlWRsoHqIyiV2v4DsmeB9OpgVeOvi2goqwFtpTivwN0ghZfUiYII013J8zhyzogyJd29UkF7YNikHYNKuCGAOIp2Q90iT3tvuCYgxb0Lv4OwcisSyJk/2RLTd/iKf5KL7x/jTuqdPyl0iG5/dL6ihRu+7E6twfDmWMauylZFtC9Fn8HMtn8T0xzT7dCKSv5n8Ueg3TaDzhnT6uJYLUwtm6rXNpwszqMqmpoctkTDGSD2mEHog6OMakok/e2o5/zmYrXguJCcK5d5hh/iPqkqgMCyAuQ1PhIQU2SF5eiwzqDv8E/kTLlSi/05iKjZsJTUJcQBoa65BhdY0oAj6hmlDjapzc4XnX8GLF9eZB2HlJLlOl/UL/DjDfe/glKskDh3x/DBOL3tGIvCIWXekLv5Z7Zy91ZcyBYvzdBY/59bFrYBIOvqVkDtsNzYEwQ2Phevw+fnDdV9zpkRVXiOAq+fKqPSsEWH6vghI+mWN8cpv2P2LOFg7Przh1c4n0UcdO+nx8g5cne9S9JvP0WQZ3vhhp8wGHUGtww/BLjsmVSQXTdVZl65ROQj7yo7CYSpEYDFAI2hnerSj2+AApRKazUeWRi3GnDyetDBAq9UZQ==

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

[Coq-Club] Domain theory in Coq, Benjamin C. Pierce, 01/05/2018
- Re: [Coq-Club] Domain theory in Coq, Robert, 01/10/2018
- <Possible follow-up(s)>
- RE: [Coq-Club] Domain theory in Coq, Moez A. AbdelGawad, 01/06/2018
  - RE: [Coq-Club] Domain theory in Coq, Nathaniel Yazdani, 01/06/2018
- Re: [Coq-Club] Domain theory in Coq, Moez A. AbdelGawad, 01/27/2018