We present {\lambda}ert, a type theory supporting refinement types with explicit proofs. Instead of solving refinement constraints with an SMT solver like DML and Liquid Haskell, our system requires and permits programmers to embed proofs of properties within the program text, letting us support a rich logic of properties including quantifiers and induction. We show that the type system is sound by showing that every refined program erases to a simply-typed program, and by means of a denotational semantics, we show that every erased program has all of the properties demanded by its refined type. All of our proofs are formalised in Lean 4.

翻译：我们提出λert，一种支持显式证明的精化类型类型理论。与通过SMT求解器（如DML和Liquid Haskell）解决精化约束不同，我们的系统要求并允许程序员在程序文本中嵌入性质证明，从而支持包含量词和归纳法的丰富性质逻辑。我们通过证明每个精化程序可擦除为简单类型程序，并借助指称语义表明每个擦除程序都满足其精化类型所要求的全部性质，以此证明类型系统的可靠性。所有证明均在Lean 4中形式化。