Skip to Content.
Sympa Menu

coq-club - Real numbers in Coq

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Real numbers in Coq


chronological Thread 
  • From: Alberto Ciaffaglione <ciaffagl AT dimi.uniud.it>
  • To: Coq club <coq-club AT pauillac.inria.fr>
  • Subject: Real numbers in Coq
  • Date: Tue, 03 Oct 2000 18:11:00 +0200

Dear All,

also here in Udine we are working on real numbers in Coq.
We have recently proposed a construction of them using
co-inductive types: we represent real numbers as streams,
a starting basis for developing constructive analysis.

Both a paper and the Coq code are available at the URL
http://www.dimi.uniud.it/~ciaffagl/C_Reals/index.html.

Best regards,

Alberto Ciaffaglione

=============================================
Alberto Ciaffaglione - Dipartimento di Matematica e Informatica
via delle Scienze, 206 - 33100 Udine (Italy)
tel: +39.0432.558469 - fax: +39.0432.558499
mailto:ciaffagl AT dimi.uniud.it
 - http://www.dimi.uniud.it/~ciaffagl
=============================================






Archive powered by MhonArc 2.6.16.

Top of Page