Valery Isaev  -  Arend proof assistant
Channel: FMF Foundations seminar
Date: 2021-11-02

Arend proof assistant

Time: Thursday, April 30, 2020
Speaker: Valery Isaev (JetBrains research)
Proof assistant: https://arend-lang.github.io/

Abstract: I will discuss Arend, a proof assistant developed at JetBrains Research. The aim of Arend is to provide a powerful system for formalization results in homotopy type theory and in ordinary mathematics. To achieve the latter goal, we prove a flexible class system with subtyping, universe polymorphism with a powerful level inference mechanism, quotient sets with a convenient pattern matching principles for them. We also recently implemented a tactic framework which can be used to automate routine proofs and implement various EDSLs. Homotopic features of Arend include built-in universes of finite homotopy level, higher inductive types, univalence, and path types in the style of cubical type theories. I will talk about these features and also about our plans to implement language extensions that can be used to simplify reasoning about various higher structures.