[l-]

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.

[EE84M3i]

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.

[1]: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.31.5... by Philip Wadler

[throwaway17_17]

For anyone interested in Wadler’s publications on Linear Logic, his homepage has a lot of pdf versions of his work in the area.

[1]: https://homepages.inf.ed.ac.uk/wadler/topics/linear-logic.ht...

[bo1024]

This is great, thanks!

[throwaway17_17]

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.