In this talk we will comment on our applied logic activities in Barcelona. We will comment on legal text analysis and the synthesis of software that is formally verified through proof assistants. In a recent project we study the Formal Requirement Elicitation Tool (FRET) of Nasa. We comment on some of our findings. We conclude by speculating on the role of Controlled Natural Languages to bridge formal reasoning with Large Language Models.

Undergrad mathematics at the University of Amsterdam with a Master in Logic at the Institute for Logic, Language and Computation; PhD at Utrecht University on Interpretability Logic; Current position at the University of Barcelona at the Philosophy Department with an ICREA Academia distinction and membership to the Institute of Mathematics of the University of Barcelona.