QArith: Coq formalisation of lazy rational arithmetic
In: TYPES 2003 : types for proofs and programs (Torino, 30 April - 4 May 2003, revised selected papers)Lecture notes in computer science; (2004) S. 309-323
Konferenz
- print, 18 ref
Zugriff:
In this paper we present the Coq formalisation of the QArith library which is an implementation of rational numbers as binary sequences for both lazy and strict computation. We use the representation also known as the Stern-Brocot representation for rational numbers. This formalisation uses advanced machinery of the Coq theorem prover and applies recent developments in formalising general recursive functions. This formalisation highlights the rôle of type theory both as a tool to verify hand-written programs and as a tool to generate verified programs.
Titel: |
QArith: Coq formalisation of lazy rational arithmetic
|
---|---|
Autor/in / Beteiligte Person: | NIQUI, Milad ; BERTOT, Yves |
Link: | |
Quelle: | TYPES 2003 : types for proofs and programs (Torino, 30 April - 4 May 2003, revised selected papers)Lecture notes in computer science; (2004) S. 309-323 |
Veröffentlichung: | Berlin: Springer, 2004 |
Medientyp: | Konferenz |
Umfang: | print, 18 ref |
ISSN: | 0302-9743 (print) |
Schlagwort: |
|
Sonstiges: |
|