Typer: a Lisp approach to dependent types

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

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

为了提高程序的可靠性和程序员的工作效率，我们需要让程序员更难以引入错误，并尽可能早地捕获这些错误。这意味着我们希望使用高级语言和库，这让程序员编写更少的代码，从而减少bug。我们希望使用测试和正式的方法来尽早发现bug。