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.