Already a while ago videolectures.net published this tutorial on Computer Verified Exact Analysis by Bas Spitters and Russell O’Connor from Computability and Complexity in Analysis 2009. I forgot to advertise it, so I am doing this now. It is about an implementation of exact real arithmetic whose correctness has been verified in Coq. Russell also [...]
|
|||||
|
These are the slides and the extended abstract from my MSFP 2008 talk. Apparently, I forgot to publish them online. There is a discussion on the Agda mailing list to which the talk is somewhat relevant, so I am publishing now. Abstract: Realizability is an interpretation of intuitionistic logic which subsumes the Curry-Howard interpretation of propositions [...] I have been writing lecture notes on computable mathematics. One of the questions that came up was whether it is possible to simulate the booleans in the simply-typed λ-calculus. This is a nice puzzle in functional programming. If you solve it, definitely let me know, although I suspect logicians did it a long time ago. I show how monads in Haskell can be used to structure infinite search algorithms, and indeed get them for free. This is a follow-up to my blog post Seemingly impossible functional programs. In the two papers Infinite sets that admit fast exhaustive search (LICS’07) and Exhaustible sets in higher-type computation (LMCS’08), I discussed what kinds [...] Lately I’ve been thinking about computational effects in general, i.e., what is the structure of the “space of all computational effects”. We know very little about this topic. I am not even sure we know what “the space of all computational effects” is. Because Haskell is very popular and in Haskell computational effects are expressed [...] HERA is an implementation of exact real arithmetic in Haskell using the approach by Andrej Bauer and Iztok Kavkler, see these and these slides. It uses the fast multiple precision floating point library MPFR. Download source, and see documentation and examples of usage at my home page. [Note by Andrej: this is a guest post by [...] Two versions of this talk were given at Computability and complexity in analysis 2008 and at Mathematics, Algorithms and Proofs 2008. Joint work with Paul Taylor. Abstract: Cauchy’s construction of reals as sequences of rational approximations is the theoretical basis for a number of implementations of exact real numbers, while Dedekind’s construction of reals as cuts has [...] Occasionally I hear claims that uncountable and uncomputable sets cannot be represented on computers. More generally, there are all sorts of misguided opinions about representations of data on computers, especially infinite data of mathematical nature. Here is a quick tutorial on the matter whose main point is: It is meaningless to discuss representations of a set [...] Andrej has invited me to write about certain surprising functional programs. The first program, due to Ulrich Berger (1990), performs exhaustive search over the “Cantor space” of infinite sequences of binary digits. I have included references at the end. A weak form of exhaustive search amounts to checking whether or not a total predicate holds for all elements of the [...] With Iztok Kavkler. Abstract: The interval domain was proposed by Dana Scott as a domain-theoretic model for real numbers. It is a successful theoretical idea which also inspired a number of computational models for real numbers. However, current state-of-the-art implementations of real numbers, e.g., Mueller’s iRRAM and Lambov’s RealLib, do not seem to be based on [...] |
|||||
|
|
|||||