By Domain Theory, I mean the use of CPOs (or related topological/order-theoretic structures) to study the denotational semantics of programming languages.

Compared to the two other common approaches to formal methods (operational and axiomatic semantics), where one might point to things like formal proof assistants, dependently-typed programming languages, refinement types, I have yet to meet a practical tool which has been developed using the tools of denotational semantics designed to formally verify real-world programs. Or, at least it seems that way on the surface.

So are they any practical formal verification tools which have benefited, either directly or indirectly, from the research into domain theory/deonotational semantics? If not, have there at least been particular software projects where the use of domain theory has helped with the process of formal verification, even if it didn't result in a general software development tool?

  • 2
    $\begingroup$ Your profile is using the Haskell logo and you are asking what domain theory has done for practical applications in formal methods? $\endgroup$ May 16 '17 at 17:48
  • $\begingroup$ @AndrejBauer at any rate, it would certainly be nice to have an overview of the relationship neatly summarized as a stackexchange answer! $\endgroup$
    – cody
    May 21 '17 at 15:19
  • $\begingroup$ I am of course aware that Haskell has a denotational semantics using domain theory. What I am looking for is practical examples, i.e. actual software projects or tools that make use of domain theory to prove that they are correct to a specification, be that formally, or informally. Searching for "domain theory formal methods" didn't seem to bring up much, and I have yet to find what I am looking for by searching for "domain theory Haskell" either, but maybe I haven't looked hard enough. $\endgroup$ May 21 '17 at 20:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.