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:

## 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

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.

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

Tipologia del documento

Tesi di laurea
(NON SPECIFICATO)

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

## Statistica sui download

Gestione del documento: