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

Date
2015
Authors
Alders, Eric
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract

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.

Description
This item is available only to currently enrolled UTSA students, faculty or staff.
Keywords
Coq, Formal Proofs, Information Flow, Programming Languages
Citation
Department
Computer Science