An Introduction to Liquid Haskell
An Introduction to Liquid Haskell
复制标题
Liquid Haskell 简介
DOI：
--
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Ricardo Peña
中科院分区：
文献类型：
--
作者：
Ricardo Peña
本文是介绍底层技术和工具Liquid Haskell的使用的教程，Liquid Haskell是函数式语言Haskell的类型检查器，可以帮助程序员以较低的工作量验证其程序的非平凡属性。
第一部分通过解释其原理并总结其类型推理算法如何证明属性来介绍Liquid Types技术。剩下的部分介绍了Haskell的一些例子，并展示了可以用这个系统证明的性质。
This paper is a tutorial introducing the underlying technology and the use of the tool Liquid Haskell, a type-checker for the functional language Haskell that can help programmers to verify non-trivial properties of their programs with a low effort.
The first sections introduce the technology of Liquid Types by explaining its principles and summarizing how its type inference algorithm manages to prove properties. The remaining sections present a selection of Haskell examples and show the kind of properties that can be proved with the system.