smljnBootstrap: new expression for running smlnj on darwin
twelf: new expression; prover for PL theory and logic