User loginNavigation |
A Certified Type-Preserving Compiler from Lambda Calculus to Assembly LanguageA Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language
I found this while attempting to follow up on this post. The approach taken here—dependently-typed ASTs and denotational semantics—and the observation that, carried to its logical conclusion, the result is typed intermediate and assembly languages, proof-carrying code, etc. suggests to me a connection to this work. It also seems to offer a denotational counterpoint to Leroy's coinductive big-step operational semantics, also done in Coq. Fascinating stuff. By Paul Snively at 2007-03-22 15:46 | Functional | Implementation | Lambda Calculus | Meta-Programming | Semantics | Type Theory | other blogs | 35355 reads
|
Browse archives
Active forum topics |
Recent comments
17 weeks 11 hours ago
17 weeks 11 hours ago
17 weeks 11 hours ago
23 weeks 21 hours ago
1 year 11 weeks ago
1 year 11 weeks ago
1 year 11 weeks ago
1 year 33 weeks ago
1 year 37 weeks ago
1 year 39 weeks ago