coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
=============================================
- Re: Real Numbers in Coq, Herman Geuvers
- <Possible follow-ups>
- Real numbers in Coq, Alberto Ciaffaglione
Archive powered by MhonArc 2.6.16.