Looking over this project, am I right in understanding that JVM bytecodes are produced directly, and thus Frege cannot be used for Android?
No, the Frege compiler produces Java code, which is translated to JVM bytecode in a later step.
Oh, cool! I'll look into this more, then, thanks :)
Actually, Gabriel Riba has managed to make an Android-App proof of concept, for more info check out the Discussion group.