User loginNavigation 
The YNot Project
This was actually commented on here, by Greg Morrisett himself. Conceptually, this seems like it's related to Adam Chlipala's A Certified TypePreserving Compiler from Lambda Calculus to Assembly Language. See, in particular, slides 2324 of this presentation (PDF). More generally, computation and reflection seem to be gaining recognition as important features for the practical use of such powerful tools as Coq; see also SSREFLECT tactics for Coq and their accompanying paper A Small Scale Reflection Extension for the Coq system (PDF). It's also interesting to observe that the work appears to depend on the "Program" keyword in the forthcoming Coq 8.2, the work behind which is known as "Russell," as referred to in this thread. Russell's main page in the meantime is here. Again, the point is to simplify programming with dependent types in Coq. Update: Some preliminary code is available from the project page. By Paul Snively at 20080129 02:14  Functional  Implementation  Semantics  Type Theory  other blogs  15339 reads

Browse archivesActive forum topicsNew forum topics 
Recent comments
6 hours 21 min ago
12 hours 9 min ago
22 hours 46 min ago
23 hours 2 sec ago
4 days 6 hours ago
4 days 9 hours ago
4 days 13 hours ago
5 days 5 hours ago
5 days 16 hours ago
1 week 6 hours ago