Formal verification of program correctness in mission critical applications is still done manually. Programming languages with dependent types used as logical frameworks present an alternative to manual verification of correctness. In this thesis we deal with type systems and programming languages with dependent types. We introduce the Idris programming language which supports arbitrarily complex dependent types. We show how to translate propositions into function types and how to prove them by implementing the functions. Correctness is then automatically verified by the compiler. With use of dependent types we provide automatically verified implementations of data structures like list, stack and queue. To demonstrate usefulness of dependent types we provide automatically verified implementation of insertion sort algorithm. We prove sortedness with linear order of natural numbers and also that the output list is a permutation of the input list. ud
展开▼
机译：关键任务应用程序中程序正确性的形式验证仍需手动完成。具有依赖类型的编程语言用作逻辑框架，是手动验证正确性的替代方法。在本文中，我们处理类型系统和具有相关类型的编程语言。我们介绍了Idris编程语言，该语言支持任意复杂的依赖类型。我们将展示如何将命题转换为功能类型，以及如何通过实现功能来证明它们。然后由编译器自动验证正确性。通过使用依赖类型，我们提供了自动验证的数据结构实现，如列表，堆栈和队列。为了证明依赖类型的有用性，我们提供了插入排序算法的自动验证实现。我们用自然数的线性顺序证明排序性，并且输出列表是输入列表的排列。 ud
展开▼
