Research
I recently completed my graduate studies in computer science at McGill University under the supervision of Prof. Zeljko Zilic at the Integrated Microsystems Laboratory. I tried 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.
Research Interests and Academic Goals
Given my background in Electrical Engineering and CS, combined with years of industry experience, I became particularly interested in the intersection of software and hardware formalization. I am currently working on a verified Hardware Description Language (HDL) built in Coq and inspired in Verilog. I am constantly asking questions about its typing system: how can I design a strongly typed language without getting rid of the comfort of writing Verilog? How can I take into account the needs for time and resource representation? More importantly, how could I properly verify the properties of this language? Is there a good semantic model for it?
I want to make Proof Assistants more accessible to a broader audience. I personally think they are awesome, and more projects could benefit from them - if we could lower the entry bar to this particular PL branch. There are many ways in which we can do it, but improving the tooling around them sounds like a good path. I threw in some of ideas in the publications list below.
Besides proof assistants and HDL, I’m broadly interested in general aspects of verification, type theory, functional programming, effective teaching of Maths, CS and Engineering.
Publications List
-
Towards an Incremental Dataset of Proofs - Human Aspects of Types and Reasoning Assistants (HATRA) 2021 (co-located with SPLASH’21 )
-
A Data-centered User Study for jsCoq - ML Workshop 2021 (co-located with ICFP’21 )
-
A Data-Centered User Study for Proof Assistant Tools - Psychology of Programming Interest Group (PPIG ) - 2021 Edition
-
Data Collection for the Learn-OCaml Programming Platform: Modelling How Students Develop Typed Functional Programs - SIGCSE’21
-
Open Source Implementations of Electromagnetic Transient Algorithms - IEEE International Conference on Industry Applications (INDUSCON )
-
Web social networks meters and business usage analysis - 2011 International Conference on Computational Aspects of Social Networks (CASoN )