Finitary-based Domain Theory in Coq: An Early Report
Moez A. AbdelGawad
TL;DR
This paper reports on formalizing finitary-based domain theory within Coq, aiming to represent finite computable objects efficiently using finitary-basis concepts.
Contribution
It introduces a formalization of domain theory in Coq utilizing finitary-basis, providing a new approach to represent finite computable objects.
Findings
Successful formalization of finitary-based domain theory in Coq
Efficient representation of finite computable objects
Foundation for further formal verification in domain theory
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsComputability, Logic, AI Algorithms · semigroups and automata theory · Logic, programming, and type systems