1 Search Results for "Prevosto, Virgile"

Document
DOI: 10.4230/DagSemProc.05021.7
Certified mathematical hierarchies: the FoCal system

Authors: Virgile Prevosto

Published in: Dagstuhl Seminar Proceedings, Volume 5021, Mathematics, Algorithms, Proofs (2006)

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.
Cite as

Virgile Prevosto. Certified mathematical hierarchies: the FoCal system. In Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, Volume 5021, pp. 1-12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@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-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.05021.7},
  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}
}
  • Refine by Author
  • 1 Prevosto, Virgile

  • Refine by Classification

  • Refine by Keyword
  • 1 Coq
  • 1 Focal
  • 1 Specifications
  • 1 computer algebra
  • 1 inheritance
  • Show More...

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2006

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact