User loginNavigation 
A Certified TypePreserving Compiler from Lambda Calculus to Assembly LanguageA Certified TypePreserving Compiler from Lambda Calculus to Assembly Language
I found this while attempting to follow up on this post. The approach taken here—dependentlytyped ASTs and denotational semantics—and the observation that, carried to its logical conclusion, the result is typed intermediate and assembly languages, proofcarrying code, etc. suggests to me a connection to this work. It also seems to offer a denotational counterpoint to Leroy's coinductive bigstep operational semantics, also done in Coq. Fascinating stuff. By Paul Snively at 20070322 15:46  Functional  Implementation  Lambda Calculus  MetaProgramming  Semantics  Type Theory  other blogs  32646 reads

Browse archivesActive forum topicsNew forum topics 
Recent comments
5 hours 20 min ago
1 week 4 days ago
1 week 6 days ago
2 weeks 6 hours ago
2 weeks 22 hours ago
2 weeks 1 day ago
2 weeks 1 day ago
2 weeks 1 day ago
2 weeks 2 days ago
2 weeks 2 days ago