A system at the cross-roads of functional and logic programming (Q1208425)

Lambda-calculus was initially designed as an alternative approach to logical foundations. After Russel's paradox this program was abandoned for it appeared as impossible to include logic inside lambda-calculus in a sound fashion. The paper is one of the recent new trials to overcome the difficulty. The idea is to build a system of types including a type \(p\) of propositions, such that the terms leading to a contradiction cannot be typed of type \(p\). This is obtained by forbidding to apply typing rules to terms of certain ``circular types''. This system includes polymorphism and is able to type for instance the fixpoint \(Y\). The soundness is not proved, but the reader is referred to another article more complete about logical properties. The paper ends with the listing of an implementation written in ML.