6 citations · 14 across the 8 of their papers we have counts for
Showing cs.LOShow all
3 papers · 1 filter
cs.LO2026
Theorem prover Arend
Fedor Part, Valery Isaev, Sergey Sinchuk
This paper is an exposition of the theorem prover Arend developed at JetBrains Research. Arend language has been designed to facilitate the formalization of mathematics within the…
cs.LO2024
(Co)condition hits the Path
Tesla Zhang, Valery Isaev
We propose an enhancement to inductive types and records in a dependent type theory, namely (co)conditions. With a primitive interval type, conditions generalize the cubical syntax…
cs.LO2020
Models of Homotopy Type Theory with an Interval Type
Valery Isaev
In this short note, we construct a class of models of an extension of homotopy type theory, which we call homotopy type theory with an interval type.