The cogent language by nicta (an easy google away) has functional semantics but uses linear logic / linear types to make sure that no gc is needed. The code is

The cogent language by nicta (an easy google away) has functional semantics but uses linear logic / linear types to make sure that no gc is needed. The code is on github and they have a very cool approach to generating proofs that any code generation maps the cogent code to equivalent c code. https://github.com/NICTA/cogent/tree/master/cogent https://github.com/NICTA/cogent/tree/master/cogent I've also been looking into how to add resource logic / linear logic to ghc Haskell / languages with a similar internal rep as ghc core. Still need to write that stuff up mind you. There's a long history of no gc free functional language research. Mlkit and clean are probably two of the older but accessible implementations in the wild