一句话：提出面向立方类型论的边界填充自动化方法，统一求解 contortion 与 Kan 问题，并实现 Haskell 求解器。
在证明助手中，立方类型论为高阶归纳类型和 univalence 提供计算支持，但其高维等式推理表现为构造给定边界的立方体，自动化困难。本文提出一个简化立方语言，分离出两类自动化问题：contortion solving（将立方体变形以适配边界）和更一般的 Kan solving（拼接多个立方体寻找解）。作者将 contortion 重述为 poset maps，从而为当前研究中最复杂的 Dedekind 与 De Morgan contortion 理论提供求解器；Kan 问题则用约束满足编程求解，且不依赖具体 contortion 理论。作者在 Haskell 中实现实验求解器，能自动求解许多立方类型论目标，并通过 Eckmann-Hilton 定理案例与基准测试验证效果。
When working in a proof assistant, automation is key to discharging routine proof goals such as equations between algebraic expressions. Homotopy type theory allows the user to reason about higher structures, such as topological spaces, using higher inductive types (HITs) and univalence. Cubical type theory provides computational support for HITs and univalence. A difficulty when working in cubical type theory is dealing with the complex combinatorics of higher structures, an infinite-dimensional generalisation of equational reasoning. To solve these higher-dimensional equations consists in constructing cubes with specified boundaries. We develop a simplified cubical language in which we isolate and study two automation problems: contortion solving, where we attempt to "contort" a cube to fit a given boundary, and the more general Kan solving, where we search for solutions that involve pasting multiple cubes together. Both problems are difficult in the general case-Kan solving is even undecidable-so we focus on heuristics that perform well on practical examples. Our language encompasses different variations of cubical type theory which differ in their "contortion theory", i.e., the class of contortions they support. We provide a solver for the contortion problem for the most complex contortion theories currently being researched, the Dedekind and De Morgan contortions, by utilizing a reformulation of contortions in terms of poset maps. We solve Kan problems using constraint satisfaction programming, which is applicable independently of the underlying contortion theory. We have implemented our algorithms in an experimental Haskell solver that can be used to automatically solve many goals a user of cubical type theory might face. We illustrate this with a case study establishing the Eckmann-Hilton theorem using our solver, as well as various benchmarks.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{DoreCM26,
title = {Automating Boundary Filling in Cubical Type Theories},
author = {Maximilian Doré and Evan Cavallo and Anders Mörtberg},
journal = {Logical Methods in Computer Science},
volume = {Volume 22, Issue 2},
year = {2026},
doi = {10.46298/lmcs-22(2:28)2026}
}