I am an MSc student at McGill university under the supervision of Prof. Zeljko Zilic at the Integrated Microsystems Laboratory. I’ve been trying to convince my lab mates that assertions are not enough to verify circuits, and we’ve been working towards a Coq implementation for verifying Verilog programs (or a subset of programs).

When I’m stuck into some arbitrary Coq proof, I usually spend some time in my side projects. One of them is thinking about better interfaces for proof assistants, and, more generally, how to make them more accessible to people.

Before that, I’ve worked with OCaml and with the LearnOCaml platform. You can check my recent poster at SIGCSE’21 here.

In the past, I also did research in an intersection of Electrical Engineering and Computer Science! More specifically, I’ve been trying to convince engineers that there are alternatives to C and C++, in particular at domains like electromagnetic transient analysis. I started with Python (in this paper), and then created some fully functional, upgraded version in Haskell.

Check my CV for further details.

Publications List

  1. Towards an Incremental Dataset of Proofs - Human Aspects of Types and Reasoning Assistants (HATRA) 2021 (co-located with SPLASH’21 )

  2. A Data-centered User Study for jsCoq - ML Workshop 2021 (co-located with ICFP’21 )

  3. A Data-Centered User Study for Proof Assistant Tools - Psychology of Programming Interest Group (PPIG ) - 2021 Edition

  4. Data Collection for the Learn-OCaml Programming Platform: Modelling How Students Develop Typed Functional Programs - SIGCSE’21

  5. Open Source Implementations of Electromagnetic Transient Algorithms - IEEE International Conference on Industry Applications (INDUSCON )

  6. Web social networks meters and business usage analysis - 2011 International Conference on Computational Aspects of Social Networks (CASoN )