The iJVM is a JVM-like machine. A state of the iJVM is a list of length 2. The first component is a call stack and the second is a class table.
(equal (car (stack (run (ijvm-fact-state n) (ijvm-fact-clock n)))) (fact n))is a theorem, where the function stack above returns the stack of the top frame and fact and ijvm-fact-state are defined as follows.
(defun fact (n) (if (zp n) 1 (* n (fact (1- n))))) (defun ijvm-fact-state (n) (make-state (push (make-frame 0 nil nil `((bipush ,n) (invokestatic "Math" "fact") (halt))) nil) (list *math-class*))) (defconst *math-class* `("Math" ("Object") (("fact" (N) ,@(ijvm-fact-program)))))