Formalizing the semantics of a dual-valued functional language in Coq

We provide the formalization, in the Coq proof assistant, of a small dual-valued functional language. Particularly, we explore the semantic properties that are required for reasoning about dual-values within a functional language. We formalize four theorems, in Coq, showing their completeness and soundness, of the small-step semantic rules for our small dual-valued functional language. We also highlight differences between the Coq implementation of our proofs from the original work done in this area by Pottier and Simonet with their Core ML2 language.