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. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Prevosto, V., & Boulmé, S. (2005). Proof contexts with late binding. In Lecture Notes in Computer Science (Vol. 3461, pp. 324–338). Springer Verlag. https://doi.org/10.1007/11417170_24
Mendeley helps you to discover research relevant for your work.