Davide Fissore
PhD student in computer science
Languages
- Italian (Native)
- French (Professional)
- English (Professional)
Interests
- Programming
- Chess
- Classic music
Career Profile
Creative and curious, I like theoretical and practical computer science. I’m interested in strongly typed programming languages which use logic or functional programming paradigms.
Education
Research in type theory through logic programming aiming to propose a versatile type-class solver for the Coq proof assistant.
Specialization in the following courses: graph theory, logic, boolean networks, type theory, complexity and constraint programming, linear programming, and artificial intelligence.
Introduction to several programming languages such as Java, Python, C, OCaml, Lisp, Javascript, MySQL. They come with other theoretical course such as data structures, language theory, network and telecommunications
Publications
-
Higher-Order unification for free!
PPDP'24
-
A new Type-Class solver for Coq in Elpi
The Coq Workshop, 2023
-
Jouer avec des Cryptarithmes en Programmation par Contraintes
JFPC, 2023 - (pag. 96-101)
Experiences
The goal of the internship is to elaborate a new type-class solver for the proof assistant Coq. The solver will be written in Elpi, a logic programming language derived from Prolog with binders and constraints which, thanks to the Coq-Elpi library can be easily plugged in the Coq’s interpreter to build new tactics and commands. This implementation aims to provide a more readable, high- customizable and user-friendly type-class solver focused on high time performances. The new solver will be tested on existing and largely used libraries in the coq world such as stdpp and iris.
Active learning with automata is a branch of language theory in which the user (learner) is capable of reconstructing the grammar G of a language via direct communication with a so-called teacher who knows G. This framework was introduced by Dana Angluin in 1987, where the learner can send to the teacher membership and equivalence queries to learn a regular grammar (this algorithm is called L*). The goal of this internship is to use this learning framework to learn more powerful grammars, in particular the visibly context- free one. An example of a grammar of this kind is represented by the XML metalanguage. You can find an implementation of mine of some the active learning algorithms I have studied here: (used technologies and frameworks: React, Redux, Bootstrap in Typescript via NodeJs)
Teaching
Projects
-
tc - A type-class solver for Coq in Elpi
A type class solver written using the coq-elpi framework (the subject of my PhD thesis)
-
Time To Tank
A 3D game written in JS using the BabylonJS framework. This game was part of a competition where we won the $2^{nd}$ price TOP du TOP (here the link of the award ceremony)
-
AllIntervalSeries
A well-known problem in constraint programming. I provide a solver written in Java using the library Choco-solver. I propose different implementations, trying to increase each time the performance of the model by attempting to break symmetries.
-
Learnng-and-More
A project where I implement in typescript different learning algorithms, ranging from the L* algorithm meant to learn regular languages to the TTT-VPA algorithm aiming to learn visible pushdown grammars.
-
Cryptator
A project on which I worked during a semester. It is a solver for cryptarithms. For this project we have published the article Jouer avec des Cryptarithmes en Programmation par Contraintes (see here)