Sciweavers

TPHOL
2009
IEEE
13 years 11 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-...
Nick Benton, Andrew Kennedy, Carsten Varming