一句话：将一大类非均匀（嵌套）数据类型与余数据类型归约到高阶逻辑中的均匀类型，并在 Isabelle/HOL 中实现。
非均匀（也称嵌套或异质）数据类型是指类型参数递归变化的数据类型，常见于 finger tree 等高效函数式数据结构的实现，但在高阶逻辑中缺乏直接支持。本文提出把一大类非均匀数据类型和余数据类型归约到均匀类型的方法，从而可在高阶逻辑中统一处理。作者在 Isabelle/HOL 证明助手中实现了该归约，扩展了其规范语言，并基于一种弱参数性变体推导出（余）归纳与（余）递归原理。该工作为在证明助手中形式化使用嵌套（余）数据结构的程序提供了基础支持。
Nonuniform (or “nested” or “heterogeneous”) datatypes are recursively defined types in which the type arguments vary recursively. They arise in the implementation of finger trees and other efficient functional data structures. We show how to reduce a large class of nonuniform datatypes and codatatypes to uniform types in higher-order logic. We programmed this reduction in the Isabelle/HOL proof assistant, thereby enriching its specification language. Moreover, we derive (co)induction and (co)recursion principles based on a weak variant of parametricity.
@inproceedings{BlanchetteM0T17,
title = {Foundational nonuniform (Co)datatypes for higher-order logic},
author = {Jasmin Christian Blanchette and Fabian Meier and Andrei Popescu and Dmitriy Traytel},
booktitle = {LICS},
year = {2017},
doi = {10.1109/lics.2017.8005071}
}