Tiago Soares

cv_f.jpg I am a PhD candidate working in colaboration with NOVA LINCS in Portugal and Inria Paris in the Cambium team. My research is conducted under the supervision of Mário Pereira and François Pottier. My work largely revolves around deductive verification and the theory of programming languages, specifically using Gospel (Generic OCaml SPEcification Language). I also like Emacs! Here's my config.

I completed the NOVA School of Science and Technology's Integrated Master's program in 2022.

Research Work

I am currently working on extending Gospel with fine grained ownership of values and support for exceptions and algebraic effects. Additionally, I am also working on translating Gospel specifications to other verification platforms, such as CFML. My research notes can be found here.

This is a continuation of the work I did during my master's thesis where, under the supervision of Mário Pereira, I created a prototype extension to the Cameleer verification tool (which uses Gospel) with support for algebraic effects and handlers leveraging defunctionalization.

This was itself a continuation of work done in my Bachelor's where I extended the Cameleer tool with support for higher order functions using defunctionalization.

Words of Wisdom

  • There can be no freedom without the abolition of the state. When there is no state, there will be freedom. - Lenin, on functional programming.
  • We're trapped in the belly of a horrible machine, and the machine is bleeding to death. - Godspeed You! Black Emperor.
  • YEAH! INCREMENTAL CHANGE! - Disco Elysium

Where you can find me

Emacs 29.3 (Org mode 9.6.15)