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  13711 reads

Browse archives
Active forum topics

Recent comments
13 weeks 5 days ago
18 weeks 18 hours ago
19 weeks 4 days ago
19 weeks 4 days ago
22 weeks 2 days ago
27 weeks 4 hours ago
27 weeks 5 hours ago
27 weeks 3 days ago
27 weeks 3 days ago
30 weeks 1 day ago