Homotopy type theory allows for a synthetic formulation of homotopy theory, where arguments can be checked by computer and automatically apply in many semantic settings. Modern homotopy theory makes essential use of the category of spectra, the natural setting in which to investigate ‘stable’ phenomena: the suspension and loop space operations become inverses. One can define a version of spectra internally to type theory, but this definition can be quite difficult to work with. In particular, there is not presently a convenient way to construct and manipulate the smash product and internal hom of such spectra. This thesis describes an extension of Martin-Löf Type Theory that is suitable for working with these constructions synthetically. There is an ∞-topos of parameterised spectra, whose objects are an index space with a family of spectra over it, so standard homotopy type theory can be interpreted in this setting. To isolate the spaces (as objects with the trivial family of spectra) and the spectra (as objects with trivial indexing space), we extend type theory with a novel modality ♮ that is simultaneously a monad and a comonad. Intuitively, this modality keeps the base of an object the same but replaces the spectrum over each point with a trivial one. The system is further extended with a monoidal tensor ⊗, unit S and internal hom ⊸, which capture abstractly the constructions on spectra mentioned above. We are lead naturally to consider a ‘bunched’ type theory, where the contexts have a tree-like structure. The modality is crucial for making dependency in these linear type formers work correctly: dependency between ⊗ ‘bunches’ is mediated by ♮. To demonstrate that this type theory is usable in practice, we prove some basic synthetic results in this new system. For example, externally, any map of spaces induces a ‘six-functor formalism’ between the categories of parameterised spectra over those spaces, and this structure can be reconstructed internal to the type theory. We additionally investigate an axiom asserting that the internal category of spectra is semiadditive; we show that in the presence of univalence this in fact implies that the category of spectra is stable.