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

<p>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. </p>

<p>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? </p>

CC BY-SA 3.0
2017-05-16T17:48:33.897Z
Your profile is using the Haskell logo and you are asking what domain theory has done for practical applications in formal methods?
Andrej Bauer
CC BY-SA 3.0
2017-05-21T15:19:26.780Z
@AndrejBauer at any rate, it would certainly be nice to have an overview of the relationship neatly summarized as a stackexchange answer!
cody
CC BY-SA 3.0
2017-05-21T20:57:33.497Z
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.
Nathan BeDell
<formal-methods><domain-theory>
Have there been any practical applications of domain theory to formal methods?
Nathan BeDell
# Have there been any practical applications of domain theory to formal methods?

(Asked by: username_0 on 2017-05-16)

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?

**Tags:** formal-methods, domain-theory

> **Comments:**
> **username_1**: Your profile is using the Haskell logo and you are asking what domain theory has done for practical applications in formal methods?  
> **username_2**: @AndrejBauer at any rate, it would certainly be nice to have an overview of the relationship neatly summarized as a stackexchange answer!  
> **username_0**: 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.  

---

## 0 answers

