Most modern programming languages include constructs for manipulating functions in a flexible way, such as passing them as parameters to other functions, storing them in heap cells, and reading/calling stored functions. These constructs are commonly used in systems code, such as Linux kernel or Apache web server, in order to implement objects or express computation that is triggered by external events. They also form a core part of high-level functional languages, such as ML and Haskell, where most of the computation is done by function manipulation. The aim of this course is to study a recent development of program logic and semantics for higher-order programs, i.e., programs that store functions in memory cells, pass them as parameters to other functions, or return them as results of function calls. The course will focus on the issues that arise from the interaction between the flexible higher-order use of functions and heap storage, and how recent results of separation logic address those issues. The topics of the course will include higher-order separation logic, higher-order frame rules, Hoare Type Theory, anti-frame rules, and the semantics of higher-order store.