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 | 34198 reads
|
Browse archivesActive forum topics |
Recent comments
7 weeks 6 days ago
8 weeks 1 day ago
8 weeks 2 days ago
15 weeks 2 days ago
21 weeks 6 hours ago
21 weeks 1 day ago
22 weeks 7 hours ago
24 weeks 5 days ago
26 weeks 1 day ago
26 weeks 1 day ago