登入選單

返回Google圖書搜尋

Comparing Intergrated [sic] and External Logics of Functional Programs

Peter Dybjer

出版	Programming Methodology Group, 1989
URL	http://books.google.com.hk/books?id=LNW-GwAACAAJ&hl=&source=gbs_api

註釋

Abstract: "Four different programming logics are compared by example. Three are versions of Martin-Löf type theory and the fourth is a version of Aczel's logical theory of constructions. They differ in several respects. For example, what is the notion of specification? Are there partial or just total objects? Is general recursion allowed or only primitive recursion of higher type? Is the logic external or integrated? The example is the proof of correctness of a normalization function for conditional expressions."