TLDR dependent lambda calculus using linear type system memory management with LLVM backend. Oddly, the source language a [dependent] lambda-calculus or a [dependent] Cartesian closed category would seem more restrictive than the linear types or closed monoidal category used to implement the compile time memory management system.
If you're not familiar with linear types, a fun paper to read is "Linear Types Can Change The World!"[1] although I might just be partial to it because of the wonderful name.
As I mentioned in another comment, the particular category he is deriving the semantic in is dictated by the CBPV semantics. I certainly agree that a closed monoidal category is the appropriate ambient category for the standard linear type theory, the structure required to reach the full semantics of CBPV, as designed by Levy, require a narrower framing. Although, it should be noted that there is only a small amount of formalism to work through and the adjunction model of CBPV can be seen as right adjoint to the linear/non-linear systems Benton describes in his 94 paper with Wadler.
