IFC is orthogonal to type systems, having also been modeled in terms of axiomatic semantics (Hoare logic) independent of a type system. It can also be practical

IFC is orthogonal to type systems, having also been modeled in terms of axiomatic semantics (Hoare logic) independent of a type system. It can also be practically implemented through runtime monitoring, partial evaluation and various hybrid approaches. Type systems are certainly one way of providing foundations for IFC, but few languages have it as a first-class construct. Notable exceptions are SPARK (based on Ada) and Jif (based on Java). See also "A Perspective on Information-Flow Control": http://www.cse.chalmers.se/~andrei/mod11.pdf http://www.cse.chalmers.se/~andrei/mod11.pdf