Sciweavers

Share
TPHOL
2009
IEEE

Some Domain Theory and Denotational Semantics in Coq

10 years 6 months ago
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.
Nick Benton, Andrew Kennedy, Carsten Varming
Added 24 May 2010
Updated 24 May 2010
Type Conference
Year 2009
Where TPHOL
Authors Nick Benton, Andrew Kennedy, Carsten Varming
Comments (0)
books