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 20090421 13:57  LtU Forum  previous forum topic  next forum topic  other blogs  7497 reads

Browse archivesActive forum topicsNew forum topics 
Recent comments
3 days 3 hours ago
3 days 5 hours ago
3 days 9 hours ago
4 days 2 hours ago
4 days 12 hours ago
6 days 2 hours ago
6 days 5 hours ago
6 days 5 hours ago
6 days 10 hours ago
6 days 10 hours ago