Argomenti di tesi proposti dal docente.
Esempi di argomenti di tesi relativi ai corsi di Logica per l'Informatica, Fondamenti Logici dell'Informatica e Paradigmi Emergenti di Programmazione:
* implementazione di un server LSP (Language Server Protocol) nel dimostratore di teoremi Matita, per consentirne l'uso tramite VSCode
* implementazione di algoritmi per la verifica di tipo, l'inferenza di tipo, la riduzione e la conversione di espressioni di linguaggi funzionali
* implementazione in Rust o in OCaml di dimostratori interattivi o automatici di teoremi
* generazione, gestione e mining di librerie di conoscenza matematica formalizzata in un dimostratore interattivo di teoremi
* visualizzazione 3D della struttura di librerie di conoscenza matematica formalizzata
Ultime tesi seguite dal docente
Tesi di Laurea
- Compilatore per linguaggio di programmazione funzionale sperimentale
- Da Matita a Dedukti e ritorno
- Il lambda-calcolo con la strategia Call-by-Value
- Logica di Hoare applicata su un
linguaggio procedurale:
implementazione Matita
Tesi di Laurea Magistrale
- Lapis-rs: a Dedukti type checker based on term graphs
