Página experimental

Pablo Benario Figueroa

Estudiante de la UChile y memorista en lenguajes de programación.

Estudio en la Universidad de Chile, en el DCC, y actualmente trabajo como memorista en el área de lenguajes de programación desarrollando una extensión de incrementalidad sobre QCheck en OCaml.

Conocer más

Explorando software

Dónde estudio

Soy estudiante de la UChile, moviéndome entre teoría, programación y sistemas desde el Departamento de Ciencias de la Computación.

En qué trabajo

Estoy haciendo mi memoria en el área de lenguajes de programación, construyendo una extensión de incrementalidad para QCheck sobre OCaml.

Qué me interesa

Me interesan los compiladores, la lógica intuicionista, los demostradores interactivos y el trabajo de bajo nivel, especialmente compilar hacia AMD64, cuando todo eso converge en la correspondencia Curry-Howard.

Intereses técnicos

Mi mayor interés es la correspondencia Curry-Howard. Cerca de eso orbitan los compiladores, la lógica intuicionista, los demostradores interactivos y el trabajo cercano a la máquina.

Rocq Asistente de pruebas y base de mucha verificación seria. Lean Lenguaje y demostrador interactivo con énfasis práctico. Agda Tipos dependientes, programación y prueba en el mismo lugar. CompCert Un compilador verificado que conecta PL y demostración. AMD64 / ABI Bajo nivel, calling conventions y cómo aterriza la compilación. QCheck Testing basado en propiedades, ahora también en mi trabajo actual.

IA y programación

Veo la IA como una herramienta para multiplicar la productividad de quienes programamos, mucho más que como una amenaza al trabajo.

Por eso me importa seguir de cerca los desarrollos más recientes y entender cómo incorporarlos con criterio en el trabajo técnico.