Typer: a Lisp approach to dependent types

Typer：一种处理依赖类型的 Lisp 方法

• 批准号: 298311-2012
• 负责人: Monnier, Stefan
• 金额: $ 1.02万
• 依托单位: Université de Montréal
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2015
• 资助国家: 加拿大
• 起止时间: 2015-01-01 至 2016-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=571469
• 关键词: Typer; Lisp; approach; dependent; types

To improve program reliability and programmer productivity, we need to make it harder for the programmer to introduce bugs, and to catch those bugs as early as possible. That implies we want to use high-level languages and libraries, which let the programmer write less code and hence fewer bugs. And we want to use testing and formal methods to catch bugs early. The more lightweight the method we use, the better, since one of the virtues of programmers is laziness. The most successful formal method around is by far type checking, as seen for example in Java. Sadly, traditional types only bring us so far. Other techniques let us catch more bugs, e.g. model checking or Hoare-style logic, but at the cost of a lot more work and expertise, leaving those techniques to niches. My research program proposes a new language Typer, which combines the pragmatic flexibility of Lisp style languages with the powerful theory of dependent types used in proof assistants. Its type system seamlessly covers the range from traditional simple type annotations to arbitrarily more complex correctness properties. This will make it easier to write and maintain software whose robustness is mechanically verified. Of course, the success of Java-style type checking does not immediately carry over to all forms of type checking. To make use of the extra power, you still need extra work, extra annotations, and extra expertise. To some extent this is unavoidable, but there is still a lot of room for improvement. So the focus of my research program is on making it easier and more incremental to use the extra power provided by advanced type systems. Formal methods have revolutionized the way hardware is designed, and the world of computer software is going through a similar transformation; leading it can bring large strategic benefits to the software industry in Canada. Another way to evaluate the impact of such a development is to look at the current vulnerability of our society as a whole to very simple computer viruses.

为了提高程序的可靠性和程序员的生产力，我们需要让程序员更难引入bug，并尽可能早地捕获这些bug。 这意味着我们希望使用高级语言和库，这可以让程序员编写更少的代码，从而减少错误。 我们希望使用测试和正式的方法来早期捕获bug。 我们使用的方法越轻量级越好，因为程序员的优点之一就是懒惰。 最成功的形式化方法是类型检查，例如在Java中。 可悲的是，传统的类型只能带我们到目前为止。 其他技术可以让我们捕获更多的错误，例如模型检查或Hoare风格的逻辑，但代价是更多的工作和专业知识，将这些技术留给利基。 我的研究计划提出了一种新的语言类型，它结合了Lisp风格语言的实用灵活性和证明助手中使用的依赖类型的强大理论。 它的类型系统无缝地覆盖了从传统的简单类型注释到任意更复杂的正确性属性的范围。 这将使编写和维护其鲁棒性经过机械验证的软件变得更容易。 当然，Java风格的类型检查的成功并不能立即推广到所有形式的类型检查。 为了利用额外的功能，您仍然需要额外的工作、额外的注释和额外的专业知识。 在某种程度上，这是不可避免的，但仍有很大的改进空间。 因此，我的研究计划的重点是使其更容易和更增量地使用高级类型系统提供的额外功能。 形式化方法已经彻底改变了硬件的设计方式，计算机软件世界也正在经历类似的转变;领导它可以为加拿大的软件行业带来巨大的战略利益。 评估这种发展的影响的另一种方法是看看我们整个社会目前对非常简单的计算机病毒的脆弱性。