Por Alcides Fonseca (Departamento de Informática and LASIGE, Faculdade de Ciências, Universidade de Lisboa, Portugal).
This talk will address the developments my research group has made in the intersection of liquid types and genetic programming. Firstly, we will address what are liquid types (integers between 3 and 5) and how they can be used for general-purpose programming. Next, we will show how these types can narrow the search space of programs in the context of program synthesis. Our goal is that developers only need to express the specification of functions (or provide examples), and the compiler will write the code for them. But unlike Github Copilot, it will be safe to use, as all properties are verified using an SMT solver.
Finally, we will show how to use these techniques to produce classifiers and regressors for real-world problems that make use of our extra expressive power to produce meaningful explanations, including those about DNA or mathematical proofs.
