Completeness, minimal logic and programs extraction
We formalize, in the AF(2)-type system, a completeness and correctness theorem for a modified Kripke semantics for minimal logic. We show that any program extracted from a proof of the completeness theorem translates higher-order encoding of a lambda -term into a Debruijn encoding of another lambda -term with the same type. We also show that any program extracted from the correctness theorem performs the reverse translation. Moreover, in both cases, there is one proof which corresponds to a program that does not change the underlying lambda -term. (C) 2001 Elsevier Science B.V. All rights reserved.
program extraction af(2)-type system types lambda-calculus intuitionnistic logic