nbe-weak-stlc Agda formalization of normalization by evaluation for the confluent simply-typed weak lambda-calculus. Companion code to my paper Normalization by Evaluation for Typed Weak lambda-Reduction (link here).