## Stuff written by other people (that I liked)
""" Bitcoin … tearfully reminds one of the old days of the pre-September Internet.
Linus “doesn't do github pull requests” and thinks it doesn't add much to git aside from hosting. I agree. “Quantum Cryptography is as awesome as it is pointless” – Bruce Schneier I've been reading a bit about Elliptic Curve Cryptography lately. Stumbled across a fantastic set of slides by Joseph H. Silverman. These slides are the only introductory material I've been able to find that touches on the question of why is it safe to use smaller keys with ECC than with the multiplicative groups of modular arithmetic or finite fields. My own interpretation of the answer is that they simply needed a group for which the index calculus algorithm doesn't work. I'm left wondering if ECC lacks efficient DLP algorithms simply because it hasn't been around as long as the other groups; apparently the crypto community has some sort of reason for thinking this isn't the case. End of Cypherpunks – A List Goes Down in Flames Scott Aaronson's witful mockery of the academic publishing companies.
""" Wait, people are still using XML? How do they get any work done?
I am resolutely opposed to that barbarous platinum-iridium relic. Let the fiat kilogram float! Facebook and twitter are nifty, but please don't call them technology companies (unless you think that MTV, Warner Brothers, and EMI are tech companies too!)
Phil Wadler's excellent Proofs are Programs: 19 John Ousterhout's Fortnight Milestones
How to get Proof General to invoke coq with
(*
*** Local Variables: *** *** coq-prog-name: "coqtop" *** *** coq-prog-args: ("-I" "." "-emacs" "-impredicative-set") *** *** End: *** *) William Wulf's Are We Scientists or Engineers? (or informaticians?).
What happened to the Berkeley Co-op? Phil Wadler's law of language design
Some objections to XML which resonate with me: C2 Wiki and IBM. Dan Bernstein's has a great analysis of IPv6.
The Two Cultures of Mathematics explains the subtle divide between “combinatorics” and logicians in some math cultures. Yaron Minksy's thoughts on how to set up distributed version control and “build daemons”. “Malcolm Gladwell is [merely] a walking Readers Digest 2.0”
Should I go to Grad School? is required reading for anybody submitting a grad school application.
Recursive ## ComputabilityAndrej Bauer's excellent description of the Kleene Tree ## Random Type Theory LinksAn example of a practical use for weakly positive (positive but not strictly-positive) types in System F.
Frank Pfenning's research on subtyping and intersection types is essential reading; although he has many papers on this subject, it seems that only this recent one gives an in-depth explanation of the Dave Menendez has a great example that nicely summarizes one of the key advantages of intersection types:
twice :: (a -> b ∧ b -> c) -> a -> b
twice f = f . f ## Hurkens ParadoxIn the Calculus of Constructions, there is a very delicate relationship between proof-irrelevance, excluded middle, and various weak axioms of choice. This relationship is most succinctly revealed by the Hurkens Paradox. There are numerous papers on this topic, but I've found only one that's approachable for a beginner: Barbanera and Berardi's Proof-irrelevance out of Excluded-middle and Choice in the Calculus of Constructions.
In particular, this paper explains how excluded middle and a strong choice axiom force proof-irrelevance. The extraction principles in ## ParsersTerrence Parr explains a problem with how PEGs “handle” (ignore?) ambiguity. This concerns me as well. I wrote a bit about it here. PEGs also have difficulties with what is called “language hiding”. Essentially, a prioritized choice
A = B / C
will never attempt to match There are two common examples of this:
A = "a" / "ab"
B = "a"* ("ab" / "c")
In both cases, the
Unfortunately, problems of this sort become much more difficult to debug in larger, more complex grammars. When grammars are built out of modules written by different authors, the problem becomes nearly intractable: imagine a production Also, as far as I know, no packrat parser currently supports indirect left recursion via grammar transformation. Packrat parsers can be modified to handle left recursion without transformation, but only by sacrificing linear time parsability. |