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 | 35049 reads
|
Browse archives
Active forum topics |
Recent comments
20 weeks 1 day ago
20 weeks 1 day ago
20 weeks 1 day ago
42 weeks 2 days ago
46 weeks 4 days ago
48 weeks 1 day ago
48 weeks 1 day ago
50 weeks 6 days ago
1 year 3 weeks ago
1 year 3 weeks ago