hide
Free keywords:
-
Abstract:
The focal language (formerly Foc) allows one to incrementally build modules and
to prove formally their correctness. focal encourages a development process by
refinement, deriving step-by-step implementations from specifications. This
refinement process is realized using an inheritance mechanism on structures
which can mix primitive operations, axioms, algorithms and proofs. Inheriting
from existing structures allows to reuse their components under some
conditions, statically checked by the compiler.
This paper presents two formal semantics for encoding focal
constructions in the Coq proof assistant. The first one is a shallow embedding
which gives a practical way to use Coq to check proofs in focal libraries. The
second one formalizes the focal structures as Coq types (called mixDrecs) and
shows that the informal semantics of focal libraries is coherent with respect
to Coq logic. In the last part of the paper, we prove that the first embedding
is conform to the mixDrecs model.
