Anzeige
Erschienen in:
2012 | OriginalPaper | Buchkapitel
Scalable Formal Machine Models
verfasst von : Greg Morrisett
Erschienen in: Programming Languages and Systems
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
In the past few years, we have seen machine-checked proofs of relatively large software systems, including compilers and micro-kernels. But like all formal arguments, the assurance gained by these mechanical proofs is only as good as the models we construct of the underlying machine. I will argue that how we construct and validate these models is of vital importance for the research community. In particular, I propose that we develop domain-specific languages (DSLs) for describing the semantics of machines, and build interpretations of these DSLs in our respective proof-development systems. This will allow us to factor out and re-use machine semantics for everything from software to hardware.