Lambda Mountain

λ☶ (pronounced Lambda Mountain) is a compiler backend. It is a typed fragment assembler, which means it could generate machine code, but right now the only backend targets GNU Assembler.

More information is available on the λ☶ Wiki.

There is also a Bootstrap Book that explains the compiler internals in great detail.

For those looking for a TLDR, this project uses the following inference rules to turn Simply Typed Lambda Calculus into a workhorse.

$$abstraction \quad \frac{\Gamma \vdash a:A \quad \Gamma \vdash b:B \quad \Gamma \vdash x:X \quad \Gamma \vdash y:Y \quad λ⟨a.b⟩⟨x.y⟩}{\Gamma \vdash λ⟨a.b⟩⟨x.y⟩:(A \to B) + (X \to Y)}$$

$$application \quad \frac{\Gamma \vdash f:(A \to B) + (C \to D) + (X \to Y) \quad \Gamma \vdash x:A + X \quad f(x)}{\Gamma \vdash f(x):B + Y}$$