3 ms·

isn't system F (with some extensions) exactly this kind of VM? some functional languages (more or less) use (something like it) as the last functional intermedi

isn't system F (with some extensions) exactly this kind of VM? some functional languages (more or less) use (something like it) as the last functional intermediate language for compilation

carnitine 5y ago
No, because System F cannot be used to express particularly interesting proofs.