Amar Hadzihasanovic: alifib: a language founded on higher-dimensional rewriting

Speaker
Amar Hadzihasanovic, Tallinn University of Technology

Abstract
I will give an introduction to alifib, an experimental programming language founded on higher-dimensional rewriting, and demonstrate a web-based proof assistant built around it; this is joint work with Alex Kavvos.
alifib implements a minimal type theory in which the only types that exist are directed higher inductive types. Terms are assembled as pasting diagrams of generators. Semantically, the types are finite directed complexes, which have a dual nature of “combinatorial cell complexes” and “higher-dimensional rewrite systems”. These are extremely versatile structures, allowing for disparate uses of the language ranging from “proof-relevant equational reasoning in categorical structures”, to “specification of abstract machines with witnesses for their computational traces” through “computation of the homology of finite cell complexes”.
Directed complexes are also the basis of the models of (infty, n)-categories which Clémence Chanavat and I used to achieve a semi-strictification theorem last year. This gives a direct avenue for translation from alifib proofs to cells in higher categories. In the context of this conference, I hope to open up an exploration of how aspects of alifib’s interactive proof development may be integrated in the workflow of other proof assistants for the formalisation of higher-categorical results.