User loginNavigation |
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? By Jason Dusek at 2009-04-21 13:57 | LtU Forum | previous forum topic | next forum topic | other blogs | 9467 reads
|
Browse archivesActive forum topics |
Recent comments
6 weeks 4 days ago
6 weeks 6 days ago
7 weeks 13 hours ago
14 weeks 11 hours ago
19 weeks 5 days ago
19 weeks 6 days ago
20 weeks 5 days ago
23 weeks 3 days ago
24 weeks 6 days ago
25 weeks 2 hours ago