Lapis-rs: a Dedukti type checker based on term graphs

Logical frameworks are formal systems that provide a meta-language for specifying and manipulating other logical systems. Logical frameworks play a crucial role in the field of formal verification: many proof assistants and proof checkers are based on these frameworks to ensure that specific properties for programs or system always hold. λΠ-calculus modulo is a modern and elegant logical framework for expressing type systems. This framework introduces the notion of dependent types, hence enabling more expressive systems. Moreover, λΠ calculus modulo introduces the notion of rewrite rules, that provide a more flexible and expressive system, particularly useful for encoding type systems. Dedukti is a logical framework that implements λΠ-calculus modulo theory. Many of the existing implementations of proof assistants and proof checkers, such as Dedukti, use de Brujin indices for representing and manipulating λ-terms. De Brujin indices provide a handy structure for handling λ terms and avoid issues such as variable renaming in many operations, such as β reduction and α-equivalence. An alternative approach to handling λ terms is given by term graphs, graph based data structures where nodes represent subterms and edges represent relations between sub-terms. Term graphs provide the ability to easily represent shared subterms with a single node: this mechanisms helps in eliminating redundancy and in handling efficiently the memory. For this reason, term graphs provide very efficient algorithms for computing operations on sub terms, such as β reduction and α-equivalence. This work aims at the implementation of a bidirectional typechecker based on term graphs, compatible with Dedukti. One important task of this thesis consists in implementing an algorithm for checking α-equivalence using sharing equality, an algorithm that uses term graphs and computes the check in linear time.