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  7139 reads

Browse archivesActive forum topics 
Recent comments
38 min 35 sec ago
2 hours 6 min ago
3 hours 41 min ago
5 hours 20 min ago
15 hours 18 min ago
15 hours 23 min ago
19 hours 26 min ago
19 hours 47 min ago
20 hours 22 min ago
20 hours 43 min ago