Spracherkennung für: vermutete Sprache: Unknown {[0] [0] [0]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen]
This folder contains a formalization of the type system, operational
semantics, and a proof of type soundness for Featherweight Java in
Isabelle/HOL. The development closely follows the proof originally
published in ACM TOPLAS.
Here is the description for each file:
- FJDefs.thy: definition of Featherweight Java syntax, type system,
and evaluation relation.
- FJAux.thy: auxiliary lemmas.
- FJSound.thy: type soundness theorems.
[Dauer der Verarbeitung: 0.25 Sekunden]
