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

Pizzo, Nicolò (2023) Lapis-rs: a Dedukti type checker based on term graphs. [Laurea magistrale], Università di Bologna, Corso di Studio in Informatica [LM-DM270]
Documenti full-text disponibili:
[thumbnail of Thesis] Documento PDF (Thesis)
Disponibile con Licenza: Creative Commons: Attribuzione - Non commerciale - Condividi allo stesso modo 4.0 (CC BY-NC-SA 4.0)

Download (815kB)

Abstract

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.

Abstract
Tipologia del documento
Tesi di laurea (Laurea magistrale)
Autore della tesi
Pizzo, Nicolò
Relatore della tesi
Scuola
Corso di studio
Indirizzo
CURRICULUM A: TECNICHE DEL SOFTWARE
Ordinamento Cds
DM270
Parole chiave
lambda pi calculus,bidirectional typechecker,term graphs
Data di discussione della Tesi
14 Dicembre 2023
URI

Altri metadati

Statistica sui download

Gestione del documento: Visualizza il documento

^