MVP Build a functional untyped lambda calculus interpreter with a visual reduction tracer. core components (lambda calculus evaluator + visualizer) proof systems dependency graphs