GitHub repository: tlively/BrainCoqulus
Primary language: Coq
Description: A formally verified compiler of untyped lambda calculus to Brainfuck