Run your research: on the effectiveness of lightweight mechanization

Full Paper: Search Google Scholar
 
Formal models serve in many roles in the programming language community. In its primary role, a model communicates the idea of a language design; the architecture of a language tool; or the essence of a program analysis. No matter which role it plays, however, a faulty model doesn't serve its purpose. One way to eliminate flaws from a model is to write it down in a mechanized formal language. It is then possible to state theorems about the model, to prove them, and to check the proofs. Over the past nine years, PLT has developed and explored a lightweight version of this approach, dubbed Redex.
 
Suggested Reading
v

Suggest a relevant paper:
Title *
Authors Pub year

 
 

Discussion


Post anonymously: (You can change the anonymity of a comment at any time.)

You must be logged in to comment. Log in


No comments yet.