Orestis is an experienced functional programmer from Athens, Greece. His weapon of choice is Haskell for general purpose programming and Agda for dependently-typed explorations and theorem proving. His interests span programming language semantics, formal verification and algorithmic music. Currently doing a PhD in the University of Edinburgh on formalizing blockchain semantics in Agda, Orestis has a MSc degree from the Utrecht University and a BSc degree from the National & Kapodistrian University of Athens.