User loginNavigation |
Towards a Mechanized Metatheory of Standard MLTowards a Mechanized Metatheory of Standard ML, Daniel K. Lee, Karl Crary, and Robert Harper.
The way that most programming languages end up working is by defining a smaller core language to which the constructions in the base language are translated. This means that you can prove the type-safety of a programming language by showing that the internal language is type safe, and that every type-correct program in the full language translates to a type-correct expression in the internal language. In this paper, the authors carried out the mechanization of a core language for SML. The next step is mechanizing the correctness of an elaborator from SML to this core language, and then full, no-foolin' SML will have a fully machine-checked correctness proof. |
Browse archivesActive forum topics |
Recent comments
2 days 5 hours ago
1 week 1 day ago
1 week 5 days ago
2 weeks 5 days ago
3 weeks 11 hours ago
3 weeks 11 hours ago
3 weeks 15 hours ago
4 weeks 11 hours ago
4 weeks 4 days ago
4 weeks 5 days ago