4 ms·
TLDR dependent lambda calculus using linear type system memory management with LLVM backend. Oddly, the source language a [dependent] lambda-calculus or a [depe
by potiuper 6y ago
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 6y agoIf 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.5002 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.31.5... by Philip Wadler
- bo1024 6y agoThis is great, thanks!
- throwaway17_17 6y agoFor 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.html https://homepages.inf.ed.ac.uk/wadler/topics/linear-logic.ht...
- throwaway17_17 6y agoAs 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.