Idea:
自动生成逆向程序
LLVM IR ⇒ Binary 的过程中自动生成 Lifting 工具？
对于可逆编程，把两个方向的程序分开写是完全没有问题的，但是一般而言程序越长越容易出错，而且也无法保证两个程序能够一一对应，因此最好可以把这个可逆的保证融入在编程语言中。这也是当下编程语言研究中的一个领域——可逆编程语言，其具体概念可以参考这篇文献：Reversible Flowchart Languages and the Structured Reversible Program Theorem。
Research:
部分可逆编程语言 Sparcl —— Wang & Matsuda
高阶双向编程语言 HOBiT —— Wang & Matsuda
透镜(Lens)是源数据对象和视图数据对象之间的一对映射。本文提出 HOBiT 语言，其中 Lenses 被表示为标准函数，透镜组合被映射到带有绑定器的语言构造。这种设计使程序员能够以灵活的函数式风格编写双向程序，同时又能充分利用 Lenses 的表现力。
提出了一个r-Turing完全可逆命令式语言的线性时间可逆自解释器。
对于可逆语言 L（即 L 程序只计算单射函数），L 程序 rint 是一个源语言 S 的一个可逆自解释器，有： [[rint]]L (p.d) = (p.d′) ⇐⇒ [[p]]S (d) = d′
本文定义了简洁的可逆语言 R-WHILE，它是一种具有树状数据结构的结构化命令式语言，使用它来构建自解释器。这种语言是基于琼斯的不可逆转的语言。
提出了两种在可逆计算背景下用于生成先序和中序二叉树标号的算法。可逆遍历直接定义了重构二叉树的逆算法，具有与可逆遍历相同的线性时间和空间需求。
本文用可逆编程语言编写遍历过程，构造过程可以定义为语言的确定性逆向语义的结果。与不可逆语言不同，所需的二叉树构造过程从用遍历过程开始就立即开始。
R-WHILE 语言 是一种通用可逆语言，这意味着它和任何可逆语言一样强大，并且允许使用动态数据结构进行可逆编程，本文对 R-WHILE 进行了扩展，使其包含可逆递归。