This is an implementation for λ○□. The system λ○□ is a λ-calculus for a kind of multi-stage programming based on linear-time temporal logic, which was proposed in
Yosihiro Yuse and Atsushi Igarashi. 2006. A modal type system for multi-level generating extensions with persistent code. In Proceedings of the 8th ACM SIGPLAN international conference on Principles and practice of declarative programming (PPDP '06). ACM, New York, NY, USA, 201-212. DOI=http://dx.doi.org/10.1145/1140335.1140360