The focal language (formerly Foc) allows a

programmer to incrementally build mathematical

structures and to formally prove 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. Inheritance from existing structures allows to reuse their components under some

conditions, which are statically checked by the compiler.

In this talk, we first present the main

constructions of the language. Then we show a

shallow embedding of these constructions in

the Coq proof assistant, which is used to check

the proofs made in Focal. Such a proof can be

either an hand-written Coq script, made in an

environment set up by the Focal compiler, or a

Coq term given the zenon theorem prover, which is partly developped within Focal. Last, we present a formalization of focal structures and show that the Coq embedding is conform to this model.