Programming on modern computer architectures requires logic to utilize both multi-threaded CPUs and accelerators such as GPUs. This can be fraught with errors relating to transmitting and accessing memory not available to all compute resources. Moreover, once the programmer writes correct code for one system, it is often slow or incorrect when run on a different architecture.  A bottom-up approach to solving this problem is reified in the C++ library Kokkos. We approach the problem top-down, distilling and generalizing concepts found therein. We design a small language, called H-IMP—which builds on an earlier model of Kokkos called MiniKokkos—with a type system that includes notions of device memory, accelerators, and safe memory access. We show that a well-typed program is safe, which in this context means that there are no heterogeneous memory errors. Our type system enables us to define a precise notion of a portable program as a program with free variables representing where data is stored and kernels are executed. Finally, we prove a portability theorem for heterogeneous programs: that the program can run safely when instantiated on a specific set of architectures.