Proof Contexts with Late Binding

8 years 12 months ago
Proof Contexts with Late Binding
Abstract. The Focal language (formerly FoC) allows one to incrementally build modules and to formally prove their correctness. In this paper, we present two formal semantics for encoding Focal constructions in the Coq proof assistant. The first one is implemented in the Focal compiler to have the correctness of Focal libraries verified with the Coq proof-checker. The second one formalizes the Focal structures and their main properties as Coq terms (called mixDrecs). The relations between the two embeddings are examined in the last part of the paper.
Virgile Prevosto, Sylvain Boulmé
Added 28 Jun 2010
Updated 28 Jun 2010
Type Conference
Year 2005
Where TLCA
Authors Virgile Prevosto, Sylvain Boulmé
Comments (0)