论文部分内容阅读
Type theory was originally proposed for the development of constructivemathematics，but it also provided a framework for computer science to combine the logic with programming language.One of the basic ideas behind type theory is the Curry-Howard isomorphism，in which a proposition corresponds to a type or a specification，and a constructive proof of the proposition corresponds to an object of the type or a program satisfying the specification.Thus to develop a computer program satisfying a specification is equivalent to construct a proof of the corresponding proposition.In this sense，type theory can also be seen as a programming language，where the correct program can be derived from the specification，and the development and verification of programs call be manipulated within the same system. In this thesis we formalize the basic operations of binary search trees and AVL trees in type theory.We give the specifications and realize them by proving the corresponding propositions，then extract the certified programs from the proofs using the Curry-Howard isomorphism.This work demonstrates a non-trivial application of the“proofs as programs”paradigm.