License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagSemProc.05021.7
URN: urn:nbn:de:0030-drops-2740
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2006/274/
Go to the corresponding Portal

Prevosto, Virgile

Certified mathematical hierarchies: the FoCal system

pdf-format:
05021.PrevostoVirgile.Paper.274.pdf (0.2 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{prevosto:DagSemProc.05021.7,
  author =	{Prevosto, Virgile},
  title =	{{Certified mathematical hierarchies: the FoCal system}},
  booktitle =	{Mathematics, Algorithms, Proofs},
  pages =	{1--12},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5021},
  editor =	{Thierry Coquand and Henri Lombardi and Marie-Fran\c{c}oise Roy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2006/274},
  URN =		{urn:nbn:de:0030-drops-2740},
  doi =		{10.4230/DagSemProc.05021.7},
  annote =	{Keywords: Specifications, proofs, inheritance, refinement, types, Focal, Coq, computer algebra, mathematics}
}

Keywords: Specifications, proofs, inheritance, refinement, types, Focal, Coq, computer algebra, mathematics
Collection: 05021 - Mathematics, Algorithms, Proofs
Issue Date: 2006
Date of publication: 16.01.2006

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI