Lambda the Ultimate

Hello all

I am searching for M.Sc thesis ideas on the intersection: Artificial intelligence, Category theory, and Programming languages. References to relevant papers will be appreciated.

Cheers

James H. Fetzer's Program Verification: The Very Idea (1988) is one of the two most frequently cited position papers on the subject of program verification. The other one is Social Processes and Proofs by De Millo, Lipton, and Perlis (1979), previously discussed on LtU. Fetzer's paper generated a lot of heated discussion, both in the subsequent issues of CACM and on Usenet.

It's not clear to me what all the fuss is about. Fetzer's main thesis seems pretty uncontroversial:

The notion of program verification appears to trade upon an equivocation. Algorithms, as logical structures, are appropriate subjects for deductive verification. Programs, as causal models of those structures, are not. The success of program verification as a generally applicable and completely reliable method for guaranteeing program performance is not even a theoretical possibility.

(See also part I, part II, and part III.)