User loginNavigation 
Theorem proving support in programming language semantics
More work on mechanized metatheory with an eye towards naturalness of representation and automation. This seems to me to relate to Adam Chlipala's work on A Certified TypePreserving Compiler from Lambda Calculus to Assembly Language, which relies on denotational semantics and proof by reflection, in crucial ways. More generally, it seems to reinforce an important trend in using typetheorybased theorem provers to tackle programming language design from the semantic point of view (see also A Very Modal Model of a Modern, Major, General Type System and Verifying Semantic Type Soundness of a Simple Compiler). I find the trend exciting, but of course I also wonder how far we can practically go with it today, given that the overwhelming majority of the literature, including our beloved Types and Programming Languages, is based on A Syntactic Approach to Type Soundness. Even the upcoming How to write your next POPL paper in Coq at POPL '08 centers on the syntactic approach. Is the syntactic approach barking up the wrong tree, in the long term? The semantic approach? Both? Neither? By Paul Snively at 20071227 22:21  Functional  Implementation  Lambda Calculus  Semantics  other blogs  11299 reads

Browse archivesActive forum topics 
Recent comments
1 week 5 days ago
1 week 5 days ago
1 week 6 days ago
1 week 6 days ago
1 week 6 days ago
1 week 6 days ago
2 weeks 1 day ago
2 weeks 2 days ago
3 weeks 15 hours ago
3 weeks 1 day ago