Finitary-based Domain Theory in Coq: An Early Report
arXiv:1801.08441
Abstract
In domain theory every finite computable object can be represented by a single mathematical object instead of a set of objects, using the notion of finitary-basis. In this article we report on our effort to formalize domain theory in Coq in terms of finitary-basis.
13 pages