Andrea discovered Haskell in 2006 through his interest into programming languages, this led him down the path of type systems research, directly contributing to the Haskell implementation of the dependently typed language Agda, in particular as main author of the Cubical Agda extension.
Andrea also worked on smart contract design and development for protocols operating on the Cardano blockchain.
He holds a PhD in Computer Science from Chalmers University, which he followed with a post-doctoral fellowship at IT University Copenhagen. He published in international conferences, including ICFP. His research focused on improving the expressivity of dependent type theory, including coinductive programming and reasoning, homotopy and cubical type theory, and modalities for parametricy and erasure. He has experience supervising students, and teaching functional programming at the undergraduates and higher levels.