| 书目名称 | Semantics of Type Theory | | 副标题 | Correctness, Complet | | 编辑 | Thomas Streicher | | 视频video | | | 丛书名称 | Progress in Theoretical Computer Science | | 图书封面 |  | | 描述 | Typing plays an important role in software development. Types can be consid ered as weak specifications of programs and checking that a program is of a certain type provides a verification that a program satisfies such a weak speci fication. By translating a problem specification into a proposition in constructive logic, one can go one step further: the effectiveness and unifonnity of a con structive proof allows us to extract a program from a proof of this proposition. Thus by the "proposition-as-types" paradigm one obtains types whose elements are considered as proofs. Each of these proofs contains a program correct w.r.t. the given problem specification. This opens the way for a coherent approach to the derivation of provably correct programs. These features have led to a "typeful" programming style where the classi cal typing concepts such as records or (static) arrays are enhanced by polymor phic and dependent types in such a way that the types themselves get a complex mathematical structure. Systems such as Coquand and Huet‘s Calculus of Con structions are calculi for computing within extended type systems and provide a basis for a deduction oriented mathematical founda | | 出版日期 | Book 1991 | | 关键词 | Mathematica; logic; programming; software development; verification | | 版次 | 1 | | doi | https://doi.org/10.1007/978-1-4612-0433-6 | | isbn_softcover | 978-1-4612-6757-7 | | isbn_ebook | 978-1-4612-0433-6 | | copyright | Springer Science+Business Media New York 1991 |
The information of publication is updating
|
|
发表于 2025-3-21 16:53:05
