A machine-checked model for a Java-like language, virtual machine, and compiler
By Gerwin Klein, Tobias Nipkow. TOPL, 2006
306 citations recorded by the source corpus.
Subfields: Artificial Intelligence, Computer Networks and Communications
View Paper: https://www.semanticscholar.org/paper/dca06df89e68c6af334a537e8190026de83a6181
How researchers see this paper
The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.
In Artificial Intelligence
- Xavier Leroy
- Tobias Nipkow
- Nate Foster
- Peter Sewell
- M. Wenzel
- Benjamin C. Pierce
- Steve Zdancewic
- Dimitrios Vytiniotis
In Computer Networks and Communications
- Xavier Leroy
- Nate Foster
- Peter Sewell
- Benjamin C. Pierce
- Steve Zdancewic
- Arjun Narayan
- Daniel Kifer
- Danfeng Zhang
Citations in the corpus
- Mechanized Metatheory for the Masses: The PoplMark Challenge (2005, methodology): “For examples, see the work on proofs of correctness of the DamasMilner type inference algorithm for ML [6, 22], semantics for C [25], semantics for Standard ML [32, 34, 13], and semantics and proofs of correctness for substantial subsets of Java [24, 17, 23].”
- A Formally Verified Compiler Back-end (2009, methodology): “Several mechanical verifications of Kildall’s worklist algorithm have been published already [5,26,49,12].”
- Formal certification of a compiler back-end or: programming a compiler with a proof assistant (2006, methodology): “Strecker [33] and Klein and Nipkow [ 15 ] certified nonoptimizing byte-code compilers from a subset of Java to a subset of the Java Virtual Machine using Isabelle/HOL.”
- The Isabelle Framework (2008, background): “Jinja has become the basis for further extensions like multithreading [25] and multiple inheritance [46].”