License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.CCA.2009.2255
URN: urn:nbn:de:0030-drops-22554
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2009/2255/
Go to the corresponding OASIcs Volume Portal

Spitters, Bas ; O'Connor, Russell
Tutorials

Computer Verified Exact Analysis (Tutorial)

pdf-format:
Spitters.2255.pdf (0.1 MB)

Abstract

This tutorial will illustrate how to use the Coq proof assistant to implement effective and provably correct computation for analysis. Coq provides a dependently typed functional programming language that allows users to specify both programs and formal proofs.

We will introduce dependent type theory and show how it can be used to develop both mathematics and programming. We will show how to use dependent type theory to implement constructive analysis. Specifically we will cover how to implement effective real numbers and effective integration.

This work will be done using the Coq proof assistant. The tutorial will cover how to use the Coq proof assistant. Attendees are encouraged to download and install Coq 8.2 from {\tt http://coq.inria.fr/download} and also download and make the full system of C-CoRN from {\tt http://c-corn.cs.ru.nl/download.html} beforehand.

BibTeX - Entry

@InProceedings{spitters_et_al:OASIcs:2009:2255,
  author =	{Bas Spitters and Russell O'Connor},
  title =	{{Computer Verified Exact Analysis (Tutorial)}},
  booktitle =	{6th International Conference on Computability and Complexity in Analysis (CCA'09)},
  series =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-12-5},
  ISSN =	{2190-6807},
  year =	{2009},
  volume =	{11},
  editor =	{Andrej Bauer and Peter Hertling and Ker-I Ko},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2009/2255},
  URN =		{urn:nbn:de:0030-drops-22554},
  doi =		{10.4230/OASIcs.CCA.2009.2255},
  annote =	{Keywords: Proof assistant, dependent type theory, constructive analysis}
}

Keywords: Proof assistant, dependent type theory, constructive analysis
Collection: 6th International Conference on Computability and Complexity in Analysis (CCA'09)
Issue Date: 2009
Date of publication: 25.11.2009

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