Unifying sets and programs via dependent types

详细信息	查看全文 | 推荐本文 |

• 作者：Wojciech Moczyd艂owski ^{wojtekm@google.com}
• 关键词：03E65 ; 03F05 ; 03F65 ; 68N18
• 刊名：Annals of Pure and Applied Logic
• 出版年：2012
• 期刊代码：4_01680072
• 类别：cp
• 出版时间：July, 2012
• 卷：163
• 期：7
• 页码：789-808
• 文件大小：305 K

摘要

We present a foundational framework, which we call D, unifying a lazy programming language with an impredicative constructive set theory IZF_R聽by means of dependent types. We show that unification brings many benefits to both worlds. First, D聽supports two paramount paradigms of creating reliable software: correctness by construction and post-construction verification, while retaining the expressiveness of set theory. Second, D聽provides new expressive power, which makes it possible to internalize and prove inside D聽the standard meta-theoretic properties of constructive systems, such as Numerical Existence Property and Program Extraction. Finally, computation arising from the programming language significantly enriches set theory, as we show that D聽is stronger than IZF_R聽and that its real numbers behave in a better way.