El 7 de julio Martín presentó el artículo "Formalization in Constructive Type Theory of the Standarization Theorem for the Lambda Calculus using Multiple Substitution” en el marco de Federated Logic Conference (FLoC) 2018, conferencia arbitrada que tuvo lugar en University of Oxford, del 6 al 19 de julio de 2018.
Ese artículo fue su tesis de maestría y es la demostración de un teorema completamente verificado en un lenguaje de programación llamado AGDA.
Según explica Martín “uno de los mayores problemas que tienen hoy en día los software son los bugs, es muy complicado hacer un programa que no tenga errores”.
Sin embargo, el lenguaje AGDA “permite producir programas más fiables y sin errores porque obliga al programador a escribir una demostración matemática de que el programa es correcto, lo cual tiene sus costos porque lleva más tiempo desarrollarlo pero también tiene sus beneficios porque, de esa manera, se asegura que el programa cumple con la especificación.
Este año la conferencia se llevó a cabo en una de las universidades más destacadas a nivel mundial y Martín tuvo la suerte de estar ahí. Además, la presentación actuó como cierre de su etapa de investigación ya que ahora está trabajando en Londres como ingeniero de software en Palantir, una compañía especializada en análisis de big data.
“Fue una preciosa experiencia, nunca había estado en Oxford y fue impresionante. Además, me permitió conocer a otras personas que están trabajando en áreas similares y generar contactos”.