PhD 的 oral exam

PhD 的 oral exam，是从一个 PhD student 变成一个 PhD candidate 需要的 “口试”。这里就是我用来口试的幻灯片，它包含了我的一些非常重要的思想和直觉。本来这些想法好些是可以作为论文题目的，现在既然我不打算要博士学位了，就把这些想法放在网上免费送人好了。不过这些恐怕要程序语言的行家才看得明白。

里面提到的内容包括：

• Some rarely known intuitions about Hindley-Milner type inference
• What is fundamentally wrong with let-polymorphism and how to fix it
• The reason why we have Curry-Howard correspondence
• The relationship between program analysis and Hoare Logic (Separation Logic)
• The relationship between Linear Logic and intersection types
• The relationship between automatic theorem proving and supercompilation

我进行这些研究的主要目的是：现在学术界有太多的概念产生，而很多概念之间其实没有本质的区别。我试图把多个重要概念统一成一个，从而降低理解的难度，节省重复劳动，促进本质性的“新发现”的产生。其实其中一些目标已经达到了，只是没有发表论文而已。