Semantics of Type Theory: Correctness, Completeness and Independence Results

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 specification. By translating a problem specification into a proposition in constructive logic, one can go one step further: the effectiveness and unifonnity of a constructive proof allows us to extract a program from a proof of this proposition. Thus by the "proposit...