What's new

Oct 22 I served on the POPL21 Artifact Evaluation Committee.
Aug 9 I joined Ilya Sergey's group at the NUS School of Computing. Very exciting!


  1. George Pîrlea and Ilya Sergey. Mechanising Blockchain Consensus. In 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018). Los Angeles, CA,USA, January 2018. ACM.


  1. CS3243 Introduction to Artificial Intelligence (AY 2020/21 Sem 2)
  2. YSC3208 Programming Language Design and Implementation (AY 2020/21 Sem 1)


  1. Toychain: Formally Verified Blockchain Consensus
    MEng Thesis. Advised by Earl Barr and Ilya Sergey.

    Abstract: We present Toychain, the first proven-correct implementation of a Nakamoto-style blockchain consensus protocol. We improve our original model by removing several overly-strong assumptions, notably the assumption that hashing is injective. Then, we instantiate the model with a SHA256-based proof-of-work scheme and extract our proven-correct OCaml implementation of Nakamoto consensus. Finally, we execute our implementation on a local area network to test its effectiveness.

Selected talks