H ? « ‹ ← → › »

Language peer sets for µJava:
Russian Federation↑
Russian Federation/2000↑
Designed 2000 ↑
2000s languages ↑
Internet↑
New internationlism↑

µJava(ID:3692/jav002)

alternate simple view
Country: Russian Federation
Designed 2000

Subset Java omitting everything but classes. The type system and semantics of this language (and a corresponding abstract Machine JVM) are formalized in the theorem prover Isabelle/HOL. Type safety both of Java and the JVM are mechanically verified.
Related languages
Isabelle/HOL → µJava   Derivation of
Java → µJava   Derivation of
References:
  • Tobias Nipkow and David von Oheimb and Cornelia Pu (0) Tobias Nipkow and David von Oheimb and Cornelia Pusch "µJava: Embedding a Programming Language in a Theorem Prover"
    Search in: Google  Google scholar  World Cat  Yahoo  Overture  DBLP  Monash bib  NZ  IEEE  ACM portal  CiteSeer  CSB  ncstrl  jstor  Bookfinder