Stuff written by other people (that I liked)

Phil Wadler's excellent  Proofs are Programs: 19^th Century Logic and 21^st Century Computing and Mike Gordon's  From LCF to HOL should be required starting points for anybody interested in programming languages and type systems.

Advice on circumventing the disadvantages of laziness in Haskell. This focuses mainly on the unpredictability of space complexity; the other major disadvantage to lazy-by-default (as I see it) is the lack of anything like a “stack trace” to include with runtime errors.

John Ousterhout's Fortnight Milestones

How to get Proof General to invoke coq with -fimpredicative-set; with newer versions of Proof General you need to put this at the end of your script:

William Wulf's  Are We Scientists or Engineers? (or informaticians?).

I, for one, believe that computing professionals need the earliest possible introduction of discrete mathematics and formal methods. … Indeed, beyond being inhospitable, we have expelled whole areas — numerical methods, libraries, and MIS, for example. If we continue this expulsion of the practical we will leave the field a barren husk. … In truth, we will not be more respected because of what we call ourselves.

 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.

Did you know that Don Knuth invented indentation-based subexpressions?

By relieving the brain of all unnecessary work, a good notation sets it free to concentrate on more advanced problems, and in effect increases the mental power of the race. — A. Whitehead, An Invitation to Mathematics

The Two Cultures of Mathematics explains the subtle divide between “combinatorics” and logicians in some math cultures.

I used to use darcs but recently switched to git. Nice quote by Norman Ramsey: “The highly touted 'theory of patches' is not published anywhere in any form that can be understood and checked by anyone with a little bit of mathematics (e.g., group theory or algebra).”

Random Type Theory Links

An 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 motivation for separating “sorts” from types.

Hurkens Paradox

In 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 Set can be viewed as a weak form of choice (definite description), and excluded middle lets one case-discriminate on whether or not a type is inhabited; this gives some intuition for the reason why -impredicative-set is incompatible with classical reasoning.

Unfortunately this article is in Volume 6 of the Journal of Functional Programming, whose online archives only include Volume 7 and later.

rendered from WIX