User loginNavigation |
archivesThe 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? |
Browse archivesActive forum topics |
Recent comments
1 day 1 hour ago
1 day 3 hours ago
17 weeks 5 days ago
17 weeks 5 days ago
17 weeks 5 days ago
23 weeks 6 days ago
1 year 12 weeks ago
1 year 12 weeks ago
1 year 12 weeks ago
1 year 34 weeks ago