具有黏合剂的通用结构的Barendregt变量约定的构造类型理论的形式化
我们引入了具有可变绑定信息的常规数据类型，为此我们定义了通用的形成，消除和归纳运算符。 然后，我们基于名称交换在整个宇宙的类型上定义通用的alpha等价关系，并得出迭代和归纳原理，这些原理可以对捕获barendregt的Variable Convention的alpha转换进行模运算。 我们实例化结果框架以获得Lambda演算和系统F，为此我们推导了alpha转换和替换组成的替换操作和替换引理。 整个工作都在构造型理论中进行，并由Agda系统进行了机器检验。
我们归纳并改进以下先前工作中开发的技术：
，应用通用编程方法来解决带有粘合剂的通用结构的形式化问题。
例子
主要用法示例是：
可以在此处以html格式浏览整个代码： : 。
作者
埃内斯托·科佩洛（Ernesto Copello）
诺拉·萨斯（No
