We present a higher order modal fixed point logic (HFL) that extends the modal mu-calculus to allow predicates on states (sets of states) to be specified using recursively defined higher order functions on predicates. The logic HFL includes negation as a first-class construct and uses a simple type system to identify the monotonic functions on which the application of fixed point operators is semantically meaningful. The model checking problem for HFL over finite transition systems remains decidable, but its expressiveness is rich. We construct a property of finite transition systems that is not expressible in the Fixed Point Logic with Chop (FLC) but which can be expressed in HFL. A similar argument is used to show that HFL is strictly more expressive, even over finite transition systems, than the restriction of HFL to any fixed order. Over infinite transition systems, we show that HFL can express bisimulation and simulation of push down automata, and any recursively enumerable property of a class of transition systems representing the natural numbers.