User loginNavigation |
archivesThe 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 Type-Preserving Compiler from Lambda Calculus to Assembly Language. See, in particular, slides 23-24 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 2008-01-29 02:14 | Functional | Implementation | Semantics | Type Theory | 24 comments | other blogs | 17896 reads
|
Browse archivesActive forum topics |
Recent comments
16 weeks 2 days ago
16 weeks 2 days ago
16 weeks 2 days ago
38 weeks 3 days ago
42 weeks 5 days ago
44 weeks 2 days ago
44 weeks 2 days ago
47 weeks 19 hours ago
51 weeks 5 days ago
51 weeks 5 days ago