archives

The deBrujin Criterion and the "LCF Approach".

The "LCF approach", as I understand that term, was Milner's insight that allowing proof development solely in terms of a particular type and its operations was a safe way to allow extension of the LCF proof system with ML.

The deBrujin criterion seems to be the same thing -- allowing proven terms to be constructed using only a safe kernel language.

What is the relationship of these two terms? Are they synonymous?