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?

## Recent comments

6 hours 6 min ago

6 hours 17 min ago

1 day 11 hours ago

6 days 18 hours ago

1 week 1 day ago

2 weeks 5 days ago

3 weeks 4 days ago

4 weeks 4 days ago

6 weeks 2 days ago

6 weeks 5 days ago