Some Domain Theory and Denotational Semantics in Coq
- Nick Benton ,
- Andrew Kennedy ,
- Carsten Varming
Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs) |
Published by Springer Verlag
We present a Coq formalization of constructive omega-cpos (extending earlier work by Paulin-Mohring) up to and including the inverse limit construction of solutions to mixed-variance recursive domain equations, and the existence of invariant relations on those solutions. We then define operational and denotational semantics for both a simply typed CBV language with recursion and an untyped CBV language, and establish soundness and adequacy results in each case.