I think I remeber seeing a paper about techniques for writing code generators in Haskell targeting stack based bytecodes that encoded bytecode sequences in a way that the typechecker could give you some sanity guarantees, ..
you don't ask a question, but I assume you'd like us to share any (partial) matches?-) perhaps the following two will get you started on references (although the encodings might be less useful for writing codegenerators than for analysing code sequences): -------------------------------------------------------------------------------- A compositional account of the Java Virtual Machine. In Proceedings of 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1999. http://research.sun.com/people/yelland/ -------------------------------------------------------------------------------- The Functions of Java Bytecode Mark P. Jones. In Proceedings of the OOPSLA '98 workshop on Formal Underpinnings of Java, Vancouver, BC, Canada, October 1998. http://www.cse.ogi.edu/~mpj/pubs/funJava.html -------------------------------------------------------------------------------- Cheers, Claus