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 [...]
|
|||||
|
In the last constructive gem we studied the exponential `2^NN` and its isomorphic copies. This time we shall compute the double exponential `2^(2^NN)` and even write some Haskell code. 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 [...] In a recent post I claimed that Python’s lambda construct is broken. This attracted some angry responses by people who thought I was confused about how Python works. Luckily there were also many useful responses from which I learnt. This post is a response to comment 27, which asks me to say more about my [...] |
|||||
|
|
|||||