Name
Abstract | ||
|---|---|---|
We present the formal description of an algorithm to filter values from an infinite steam using a type theory based prover. The key aspect is that filters are partial co-recursive functions and we solve the problem of expressing partiality. We then show how to prove properties of this filter algorithm and we study an application computing the stream of all prime numbers. |
Year | DOI | Venue |
|---|---|---|
2005 | 10.1007/11417170_9 | TLCA |
Keywords | Field | DocType |
coinductive stream,prime number,type theory,partial co-recursive function,formal description,filter algorithm,infinite steam,key aspect | Sieve of Eratosthenes,Lambda calculus,Prime number,Computer science,Proof theory,Type theory,Algorithm,Coinduction,Sieve,Gas meter prover | Conference |
Volume | ISSN | ISBN |
3461 | 0302-9743 | 3-540-25593-1 |
Citations | PageRank | References |
22 | 0.98 | 15 |
Authors | ||
1 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Yves Bertot | 1 | 442 | 40.82 |