Some Domain Theory and Denotational Semantics in Coq

Abstract. We present a Coq formalization of constructive ω-cpos (extending earlier work by Paulin-Mohring) up to and including the inverselimit 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 simplytyped CBV language with recursion and an untyped CBV language, and establish soundness and adequacy results in each case.

• Type: Conference
• Year: 2009
• Where: TPHOL
• Authors: Nick Benton, Andrew Kennedy, Carsten Varming
• Keywords: Artificial Intelligence, CBV Language, Recursive Domain Equations, TPHOL 2009, Untyped Cbv Language