Contact information
School of Computing National University of Singapore COM1, 13 Computing Drive Singapore 117417

1
Education and Qualifications
• Ph.D. in Computer Science, KU Leuven, Leuven, Belgium. November 2012. Thesis: Operational Aspects of Type Systems, Advisor: Dave Clarke • M.Sc. in Mathematics and Computer Science, GPA 5.0/5.0, Saint Petersburg State University, Saint Petersburg, Russia. June 2008. Thesis: Extraction of Musical Notation from a Musical Signal, Advisor: Andrey E. Barabanov
2
Employment History
•  National University of Singapore, School of Computing and Yale-NUS College (till May 2025), Singapore • Associate Professor (with tenure), July 2021–present. • Associate Professor (non-tenured, on tenure track), November 2018–June 2021. • University College London, Department of Computer Science. London, UK • Associate Professor. Effective 1 October 2018, honorary position since 1 November 2018. • Lecturer (Assistant Professor). November 2015–September 2018. • Facebook, Inc., Static Analysis Tools. London, UK Research Scientist (Part-Time). November 2017–July 2018. ・IMDEA Software Institute, Madrid, Spain Post-doctoral Researcher. February 2013–October 2015. •  Microsoft Research, Cambridge, UK Research Intern. Programming Principles and Tools group. July–September 2012. •  JetBrains Inc., Saint Petersburg, Russia Software Engineer. IntelliJ IDEA team. September 2006–November 2008.
3
Advisory Appointments and Knowledge Transfer
• Mysten Labs. Research Consultant. May 2024–present • Zilliqa Inc. Research Advisor and Lead Language Designer. March 2018–April 2024
4
Awards and Honours
•  Faculty Teaching Excellence Award (2022/2023), NUS School of Computing, 2024 • Google Research Award (South Asia & Southeast Asia) , Google Inc., 2023 • Faculty Teaching Excellence Award (2021/2022), NUS School of Computing, 2023 •  Amazon Research Award, Amazon Inc., 2022 • Distinguished Researcher Award , Yale-NUS College, 2021 •  Dahl-Nygaard Junior Prize , Association Internationale pour les Technologies Objets (AITO), 2019 • Google Faculty Research Award , Google Inc., 2017 •  Academic Excellence Scholarship , Vladimir Potanin Foundation, 2004–2007
Distinguished Papers and Software
•  Distinguished Paper Award, CPP [C35], 2024 • ACM SIGPLAN Distinguished Paper Award , PLDI [C32], 2023 ・ Distinguished Artifact Award , PLDI [ C31 ], 2023 •  ACM SIGPLAN Distinguished Paper Award , PLDI [C27], 2021 •  Distinguished Artifact Award , OOPSLA [C23], 2019 ・ACM SIGPLAN Distinguished Paper Award , POPL [C20], 2019
5

Journal articles
J6  Hippodrome: Data Race Repair using Static Analysis Summaries Andreea Costea, Abhishek Tiwari, Sigmund Chianasta, Kishore R, Abhik Roychoudhury, and Ilya Sergey ACM Transactions on Software Engineering and Methodology , volume 32, number 2, pages 41:1–41:33, 2023. J5  Protocol Combinators for Modeling, Testing, and Execution of Distributed Systems Kristoffer Just Arndal Andersen and Ilya Sergey Journal of Functional Programming, volume 31, February 2021. J4  QED at Large: A Survey of Engineering of Formally Verified Software Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, and Zachary Tatlock Foundations and Trends in Programming Languages, Volume 5, Issue 2-3, September 2019. J3  Modular, Higher-Order Cardinality Analysis in Theory and Practice Ilya Sergey, Dimitrios Vytiniotis, Joachim Breitner, and Simon Peyton Jones Journal of Functional Programming, volume 27, e11, January 2017. J2  Pushdown Flow Analysis with Abstract Garbage Collection J. Ian Johnson, Ilya Sergey, Christopher Earl, Matthew Might, and David Van Horn Journal of Functional Programming, volume 24, issue 2-3, pages 218–283, May 2014. J1  A correspondence between type checking via reduction and type checking via evaluation Ilya Sergey and Dave Clarke Information Processing Letters, volume 112, issue 1-2, pages 13–20, January 2012.
Articles in international conference proceedings
C41  Concurrent Data Structures Made Easy Callista Le, Kiran Gopinathan, Koon Wen Lee, Seth Gilbert, and Ilya Sergey Proc. ACM Program. Lang. (OOPSLA 2024) C40  DSLs in Racket: You Want It How, Now? Yunjeong Lee, Kiran Gopinathan, Ziyi Yang, Matthew Flatt, Ilya Sergey SLE 2024 C39  Compositional Verification of Composite Byzantine Protocols Qiyuan Zhao, George Pîrlea, Karolina Grzeszkiewicz, Seth Gilbert, and Ilya Sergey CCS 2024 C38  Higher-Order Specifications for Deductive Synthesis of Programs with Pointers David Young, Ziyi Yang, Ilya Sergey, and Alex Potanin ECOOP 2024 C37  Mechanised Hypersafety Proofs about Structured Data Vladimir Gladshtein, Qiyuan Zhao, Willow Ahrens, Saman Amarasinghe, and Ilya Sergey Proc. ACM Program. Lang. (PLDI 2024) C36  Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic Qiyuan Zhao, George Pîrlea, Zhendong Ang, Umang Mathur, and Ilya Sergey CPP 2024. Distinguished Paper Award C35  Greybox Fuzzing of Distributed Systems Ruijie Meng, George Pîrlea, Abhik Roychoudhury, and Ilya Sergey CCS 2023 C34  Adventure of a Lifetime: Extract Method Refactoring for Rust Sewen Thy, Andreea Costea, Kiran Gopinathan, and Ilya Sergey Proc. ACM Program. Lang. (OOPSLA 2023) C33  Mostly Automated Proof Repair for Verified Libraries Kiran Gopinathan, Mayank Keoliya, and Ilya Sergey Proc. ACM Program. Lang. (PLDI 2023). ACM SIGPLAN Distinguished Paper Award C32  Leveraging Rust Types for Program Synthesis Jonas Fiala, Shachar Itzhaky, Peter Müller, Nadia Polikarpova, and Ilya Sergey Proc. ACM Program. Lang. (PLDI 2023). Distinguished Artifact Award C31  Random Testing of a Higher-Order Blockchain Language (Experience Report) Tram Hoang, Anton Trunov, Leonidas Lampropoulos, and Ilya Sergey Proc. ACM Program. Lang. (ICFP 2022) C30  Certifying the Synthesis of Heap-Manipulating Programs Yasunari Watanabe, Kiran Gopinathan, George Pirlea, Nadia Polikarpova, and Ilya Sergey Proc. ACM Program. Lang. (ICFP 2021) C29  Practical Smart Contract Sharding with Ownership and Commutativity Analysis George Pîrlea, Amrit Kumar, and Ilya Sergey PLDI 2021 C28  Cyclic Program Synthesis Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben N. S. Rowe, and Ilya Sergey PLDI 2021. ACM SIGPLAN Distinguished Paper Award C27  Automated Repair of Heap-Manipulating Programs using Deductive Synthesis Thanh-Toan Nguyen, Quang-Trung Ta, Ilya Sergey, and Wei-Ngan Chin VMCAI 2021 C26  Certifying Certainty and Uncertainty in Approximate Membership Query Structures Kiran Gopinathan and Ilya Sergey CAV 2020 C25  Concise Read-Only Specifications for Better Synthesis of Programs with Pointers Andreea Costea, Amy Zhu, Nadia Polikarpova, and Ilya Sergey ESOP 2020 C24  Safer Smart Contract Programming with Scilla Ilya Sergey, Vaivaswatha Nagaraj, Jacob Johannsen, Amrit Kumar, Anton Trunov, Ken Chan Guan Hao Proc. ACM Program. Lang. (OOPSLA 2019). Distinguished Artifact Award C23  Running on Fumes: Preventing Out-of-Gas Vulnerabilities in Ethereum Smart Contracts using Static Resource Analysis Elvira Albert, Pablo Gordillo, Albert Rubio, and Ilya Sergey VECoS 2019 C22  Exploiting The Laws of Order in Smart Contracts Aashish Kolluri, Ivica Nikolić, Ilya Sergey, Aquinas Hobor, and Prateek Saxena ISSTA 2019 C21  Structuring the Synthesis of Heap-Manipulating Programs Nadia Polikarpova and Ilya Sergey Proc. ACM Program. Lang. (POPL 2019). ACM SIGPLAN Distinguished Paper Award C20  A True Positives Theorem for a Static Race Detector Nikos Gorogiannis, Peter O’Hearn, and Ilya Sergey Proc. ACM Program. Lang. (POPL 2019) C19  Distributed Protocol Combinators Kristoffer Just Arndal Andersen and Ilya Sergey PADL 2019 C18  RacerD: Compositional Static Race Detection Sam Blackshear, Nikos Gorogiannis, Peter O’Hearn, and Ilya Sergey Proc. ACM Program. Lang. (OOPSLA 2018) C17  Finding the Greedy, Prodigal, and Suicidal Contracts at Scale Ivica Nikolić, Aashish Kolluri, Ilya Sergey, Prateek Saxena, and Aquinas Hobor ACSAC 2018 C16  EthIR: A Framework for High-Level Analysis of Ethereum Bytecode Elvira Albert, Pablo Gordillo, Benjamin Livshits, Albert Rubio, and Ilya Sergey ATVA 2018 C15  Paxos Consensus, Deconstructed and Abstracted Álvaro García Pérez, Alexey Gotsman, Yuri Meshman, and Ilya Sergey ESOP 2018 C14  Mechanising Blockchain Consensus George Pîrlea and Ilya Sergey CPP 2018 C13  Programming and Proving with Distributed Protocols Ilya Sergey, James R. Wilcox, and Zachary Tatlock Proc. ACM Program. Lang. (POPL 2018) C12  Concurrent Data Structures Linked in Time Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski and Anindya Banerjee ECOOP 2017. C11  Programming Language Abstractions for Modularly Verified Distributed Systems James R. Wilcox, Ilya Sergey, and Zachary Tatlock. SNAPL 2017. C10  Hoare-style Specifications as Correctness Conditions for Non-linearizable Concurrent Objects Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee, and Germán Andrés Delbianco OOPSLA 2016 C9  Experience Report: Growing and Shrinking Polygons for Random Testing of Computational Geometry Algorithms Ilya Sergey ICFP 2016 C8  Mechanized Verification of Fine-grained Concurrent Programs Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee PLDI 2015 C7  Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee ESOP 2015 C6  Communicating State Transition Systems for Fine-Grained Concurrent Resources Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, and Germán Andrés Delbianco ESOP 2014 C5  Modular, Higher-Order Cardinality Analysis in Theory and Practice Ilya Sergey, Dimitrios Vytiniotis, and Simon Peyton Jones POPL 2014 C4  Monadic Abstract Interpreters Ilya Sergey, Dominique Devriese, Matthew Might, Jan Midtgaard, David Darais, Dave Clarke, and Frank Piessens PLDI 2013 C3  Introspective Pushdown Analysis of Higher-Order Programs Christopher Earl, Ilya Sergey, Matthew Might and David Van Horn ICFP 2012 C2  Calculating Graph Algorithms for Dominance and Shortest Path Ilya Sergey, Jan Midtgaard and Dave Clarke MPC 2012 C1  Gradual Ownership Types Ilya Sergey and Dave Clarke ESOP 2012 Selected peer-reviewed articles in international workshop proceedings W7  Towards Mechanising Probabilistic Properties of a Blockchain Kiran Gopinathan and Ilya Sergey. CoqPL 2019. W6  A Concurrent Perspective on Smart Contracts Ilya Sergey and Aquinas Hobor. 1st Workshop on Trusted Smart Contracts (WTSC 2017). W5  Deriving Interpretations of the Gradually-Typed Lambda Calculus Álvaro García Pérez, Pablo Nogueira and Ilya Sergey. PEPM 2014. W4  Fixing Idioms – A recursion primitive for applicative DSLs Dominique Devriese, Ilya Sergey, Dave Clarke and Frank Piessens. PEPM 2013 . W3  From type checking by recursive descent to type checking with an abstract machine Ilya Sergey and Dave Clarke. LDTA 2011. W2  Automatic refactorings for Scala programs Ilya Sergey, Dave Clarke and Alexander Podkhalyuzin The First Scala Workshop — Scala Days 2010 W1  A semantics for context-oriented programming with layers Dave Clarke and Ilya Sergey. COP 2009.
Invited articles
I2  Deductive Synthesis of Programs with Pointers: Techniques, Challenges, Opportunities Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben N. S. Rowe, and Ilya Sergey CAV 2021 I1  Temporal Properties of Smart Contracts Ilya Sergey, Amrit Kumar and Aquinas Hobor. ISOLA 2018 , The track on Reliable Smart Contracts.
Selected technical reports and software specifications
T3  Compiling a Higher-Order Smart Contract Language to LLVM Vaivaswatha Nagaraj, Jacob Johannsen, Anton Trunov, George Pirlea, Amrit Kumar, and Ilya Sergey. Extended talk abstract, accepted to the 2020 Virtual LLVM Developers' Meeting (LLVM 2020). https://arxiv.org/abs/2008.05555 T2  SCILLA: a Smart Contract Intermediate-Level LAnguage Ilya Sergey, Amrit Kumar and Aquinas Hobor. http://arxiv.org/abs/1801.00687 T1  Operational Aspects of C/C++ Concurrency Anton Podkopaev, Ilya Sergey and Aleksandar Nanevski. http://arxiv.org/abs/1606.01400
Monographs
M1  Programs and Proofs: Mechanizing Mathematics with Dependent Types Ilya Sergey. 2014. Lecture notes with exercises, available at http://ilyasergey.net/pnp .
Book chapters
B2  The Next 700 Smart Contract Languages Ilya Sergey. Principles of Blockchain Systems, Synthesis Lectures on Computer Science, Morgan & Claypool, 2021. B1  Ownership Types: A Survey Dave Clarke, Johan Östlund, Ilya Sergey and Tobias Wrigstad. Aliasing in Object-Oriented Programming: Types, Analysis and Verification, Springer, 2013.
Grants and External Research Funding
6

7
Keynote Talks at Conferences and Workshops
International Events
1. April 2022. 13th Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software (PLACES 2022), Munich, Germany. Talk title:   Growing a Smart Contract Language for a High-Throughput Blockchain 2. October 2019. 1st Workshop on Formal Methods for Blockchains (FMBC 2019), Porto, Portugal. Talk title: The Scilla Journey: From Proof General to Thousands of Nodes 3. August 2019. The 2019 ACM Symposium on Principles of Distributed Computing (PODC 2019). Toronto, Canada. Talk title: Engineering Distributed Systems that We Can Trust (and Also Run) 4. July 2019. 33rd European Conference on Object-Oriented Programming (ECOOP 2019), London, UK. Talk title: Composing Distributed Systems that are Provably Correct 5. September 2013. 15th International Symposium on Principles and Practice of Declarative Programming (PPDP 2013), Madrid, Spain. Talk title: Monadic Abstract Interpreters
National Events
1. April 2022. Seventh Conference on Software Engineering and Information Management (SEIM 2022) Russia. The conference took place virtually. https://seim-conf.org/en/ Talk title: Deductive Synthesis of Heap-Manipulating Programs: Sound, Expressive, Fast 2.  November 2020. XI Workshop Program Semantics, Specification and Verification: Theory and Applications A.P. Ershov Institute of Informatics Systems, Russia. https://persons.iis.nsk.su/en/pssv2020 Talk title: Structuring the Synthesis of Heap-Manipulating Programs 3. September 2020 . The 4th Working Formal Methods Symposium (Virtual) Faculty of Mathematics and Computer Science, Babes-Bolyai University, Romania. http://www.cs.ubbcluj.ro/from2020/ Talk title: Structuring the Synthesis of Heap-Manipulating Programs 4.  April 2017. Russian National Conference on Programming Languages and Compilers Rostov-on-Don, Russia. http://plc.sfedu.ru Talk title: Dependent Types for Verification of Real-World Programs
8
Teaching
Teaching at NUS School of Computing and Yale-NUS College

* designed new syllabus

Teaching at University College London
Teaching at KU Leuven

Teaching at Graduate Summer/Winter Schools
• SIGPL Summer School 2018, August 2018, Dongguk University, Seoul, Korea. Summer School Lecturer (gave 3 lectures on distributed systems). • Programs and Proofs: Mechanizing Mathematics with Dependent Types, August 2014, Saint Petersburg State University, Saint Petersburg, Russia. Course Designer, Summer School Lecturer (5-day course).
9
Academic Supervision
PhD students
Current PhD students •  Qiyuan Zhao , PhD student, NUS School of Computing. Since January 2023. • Yuxi Ling , PhD student, NUS School of Computing. Since January 2023. • Vladimir Gladshtein , PhD student, NUS School of Computing. Since August 2022. • Ziyi Yang , PhD student, NUS School of Computing. Since August 2021. • Yunjeong Lee , PhD student, NUS School of Computing. Since August 2020. • George Pîrlea , PhD student, NUS School of Computing. Since August 2020.
Graduated PhD students
•  Kiran Gopinathan , PhD student, NUS School of Computing, 2019-2024. Thesis: Scaling the Evolution of Verified Software. August 2024.
Postdocs
• Yutaka Nagashima , Research Associate, Yale-NUS College and NUS SoC. December 2020–January 2022. • Thomas Sibut-Pinote , Research Associate, UCL. November 2017–August 2018.
Graduated MSc Students
• Tram Hoang Ngoc , MComp student at NUS School of Computing, 2021/22. Thesis: Testing Static Program Analyses with a State-Collecting Monadic Definitional Interpreter. • Bryan Tan Yao Hong , MComp student at NUS School of Computing, 2021/22. Thesis: From C towards Idiomatic & Safer Rust through Constraints-Guided Refactoring. •  Yasunari Watanabe , MComp student at NUS School of Computing, 2020/21. Thesis: A Framework for Certified Program Synthesis. • George Pîrlea , MEng student at UCL, 2018/19. Thesis: Toychain: Formally Verified Blockchain Consensus.
Graduated Final-Year Project Advisees
• Callista Le, Capstone student at Yale-NUS College, 2023/24. Thesis: Simple and Efficient Concurrent Search Structures via Batch Parallelism. •  Nay Chi Wint Naing, Capstone student at Yale-NUS College, 2023/24. Thesis: Program Synthesis with Accumulators. •  Sewen Thy, Capstone student at Yale-NUS College, 2022/23. Thesis: Borrowing without Sorrowing: Implementing Extract Method Refactoring for Rust. Outstanding Yale-NUS Capstone Prize for 2023 • Karolina Grzeszkiewicz , Capstone student at Yale-NUS College, 2022/23. Thesis: Formally Verifying Accountable Byzantine Consensus. • Koon Wen Lee , Capstone student at Yale-NUS College, 2022/23. Thesis: Concurrent Structures and Effect Handlers: A Batch Made in Heaven. •  Mayank Keoliya , FYP student at NUS School of Computing, 2022/23. Thesis: Improving Rust Performance by Type-Directed Refactoring. • Theodore Leebrant , FYP student at NUS School of Computing, 2022/23. Thesis: Improving Rust Performance by Type-Directed Refactoring. • Juwon Lee , Capstone student at Yale-NUS College, 2021/22. Thesis: Synthesizing Musical Harmony using Equality Graphs. • Mark Weilong Yuen, Capstone student at Yale-NUS College, 2021/22. Thesis: Verifying Distributed Protocols: From Executable to Decidable. • Tram Hoang Ngoc , Capstone student at Yale-NUS College, 2020/21. Thesis: Testing Static Code Analyses with Monadic Definitional Interpreters. •  Nicholas Chin Jian Wei , Capstone student at Yale-NUS College, 2020/21. Thesis: Towards Locally-Parallel Processing of Smart Contract Transactions. • Alaukik Nath Pant , Capstone student at Yale-NUS College, 2020/21. Thesis:  Towards User-Friendly Linearizability Checking. • Gabriel Phoenix Petrov , Capstone student at Yale-NUS College, 2020/21. Thesis: A Study of Control and Type-Flow Analyses for Higher-Order Programming Languages. • Bryan Tan Yao Hong, Capstone student at Yale-NUS College, 2020/21. Thesis:  Towards Enhancing Deductive Synthesis of Heap-Manipulating Programs with Examples. • Yasunari Watanabe , Capstone student at Yale-NUS College, 2019/20. Thesis: Building a Certified Program Synthesizer. Outstanding Yale-NUS Capstone Prize for 2020 • Daniel Lok Yu-Kin , Capstone student at Yale-NUS College, 2018/19. Thesis: Modelling and Testing Composite Byzantine-Fault Tolerant Consensus Protocols. •  Jake (Si Yuan) Goh , Capstone student at Yale-NUS College, 2018/19. Thesis: Synchronisation Primitives for Smart Contracts. • Anirudh Pillai, BSc student at UCL, 2017/18. Final Year Thesis: Mechanised Verification of Paxos-Like Consensus Protocols.
Interns and Undergraduate Researchers
・ Sean Wang (undergrad at Cornell), Intern at NUS SoC, 2024. • Vikram Goyal , Research Assistant at NUS SoC, 2024. • Mayank Keoliya , Research Assistant at NUS SoC, Summer 2022–Spring 2023. Topic: Invariant Synthesis for Automated Proof Repair; conference paper: [C32] NUS Outstanding Undergraduate Researcher Award for 2023 •  Irina Artemeva , Intern at Yale-NUS College/NUS SoC, September 2020–December 2020. •  Amy Zhu (undergrad at UBC), Intern at Yale-NUS College/NUS SoC, May–August 2019. Topic: Deductive Synthesis with Read-Only Annotations; conference paper: [C24]. •  Bryan Tan , Intern at Zilliqa, May–August 2019. Topic: Compiling Scilla to SMT constraints • Kristoffer Just Andersen (Aarhus U.), Visiting PhD Researcher at UCL, January–June 2018. Topic: Practical programming with distributed protocols; papers: [ C18 , J5 ]. • Kiran Gopinathan , Intern at UCL, Summer 2018. Topic: Probabilistic reasoning about blockchain protocols; workshop paper: [W7]. •  Oscar King, Intern at UCL, Summer 2018. Topic: Extraction for verified blockchain protocols. • George Pîrlea , Intern at UCL, Summer 2017. Topic: Verification of blockchain consensus protocols in Coq; conference paper: [ C13 ]. •  Benedict Loh , Intern at UCL, Summer 2017. Topic: Implementing a program synthesis engine, based on Separation Logic. • Georgi Georgiev , Intern at UCL, Summer 2016. Topic: Verification of a concurrent garbage collector in the Coq proof assistant. •  Anton Podkopaev , Intern at IMDEA Software Institute (main supervisor: Aleks Nanevski), 2015. Topic: Operational semantics for C/C++11 concurrency; technical report: [T1]. 10
Hosted Long-Term Academic Visitors
•  Peter Müller (ETH Zurich), February–March 2024. •  Matthew Flatt (University of Utah), August 2022–May 2023, on sabbatical at NUS School of Computing. 11
Service to the Research Community
Member of Executive and Steering Committees
•  ACM SIGPLAN, Executive Committee -  Member at large, 2025–2027 • ACM SIGPLAN International Conference on Functional Programming (ICFP), Steering Committee -  ICFP'25 General Chair and Member at Large, 2025–2027 -  Publicity Chair, 2022–2024 • ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Steering Committee -  Member at large, 2022–2025 • ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), Steering Committee -  Industrial Relation Chair, 2022–2025 • European Joint Conferences on Theory and Practice of Software (ETAPS) -  Steering Committee Member, 2021–2025 •  Asian Association for Foundation of Software (AAFS) -  Executive Committee Member
International Conference Chair
• 30th International Conference on Functional Programming (ICFP 2025) General Chair • 26th International Symposium on Practical Aspects of Declarative Languages (PADL 2024) Programme Committee Co-Chair (with Martin Gebser) • 20th Asian Symposium on Programming Languages and Systems (APLAS 2022) Programme Committee Chair • 31st European Symposium on Programming (ESOP 2022) Programme Committee Chair
Workshop Chair/Organiser
• RTFM 2024: Red-Hot Topics in Faculty Mentoring (co-located with PLDI'24) June 2024, Copenhagen, Denmark. Co-Chair (with Amal Ahmed and Derek Dreyer). • Dagstuhl Seminar 23112 on Unifying Formal Methods for Trustworthy Distributed Systems March 2023, Schloss Dagstuhl, Germany. Co-Organiser (with Swen Jacobs, Kenneth McMillan, and Roopsha Samanta) • The Fifth International Workshop on Coq for Programming Languages (CoqPL 2019) January 2019, Lisbon, Portugal. Co-Chair (with Robbert Krebbers) • The Fourth International Workshop on Coq for Programming Languages (CoqPL 2018) January 2018, Los Angeles, CA, USA. Co-Chair (with Yves Bertot) •  6th South of England Regional Programming Language Seminar (S-REPLS 6) May 2017, London, UK. Organiser. Event web page: http://srepls6.cs.ucl.ac.uk. The meeting has attracted speakers from 10 institutions from France, New Zealand, Singapore, UK, USA, and has been attended by approximately 90 researchers, students, and industry practitioners.
Large-Scale Event Organiser
• ICFP Programming Contest 2019, Organiser. https://icfpcontest2019.github.io The contest took place on June 21-24, 2019. 194 teams from 25 countries have participated.
PhD Examiner
•  Ruomu Hou. NUS School of Computing, Singapore, 2024. Thesis:  Techniques For Enhancing Robustness Of Permissionless Distributed Systems • Abel Nieto Rodriguez. Aarhus University, Denmark, September 2023. Thesis: Conflict-free Replicated Data Types have Abstract Data Types • Palina Tolmach. Nanyang Technological University, Singapore, May 2023. Thesis: Securing Smart Contracts with Formal Verification and Automated Program Repair • Wei Quan Lim. NUS School of Computing, Singapore, March 2023. Thesis: Multithreaded Parallel Data Structures • Samuel Steffen. ETH Zurich, Switzerland, December 2022. Thesis: A Programming Language Approach to Smart Contract Privacy •  Xiang Gao. NUS School of Computing, Singapore, June 2021. Thesis: Over-Fitting in Program Repair and Synthesis • Ranadeep Biswas. Université de Paris, IRIF, France, March 2021. Thesis: Automated Formal Testing of Storage Systems and Applications • Marco Vassena. Chalmers University of Technology, Sweden, February 2019. Thesis:  Verifying Information Flow Control Libraries • Morten Krogh-Jespersen. Aarhus University, Denmark, December 2018 Thesis: Towards Modular Reasoning for Stateful and Concurrent Programs.
Programme Committee Member for International Conferences
• OOPSLA 2023: 37th ACM Intl. Conf. on Object-Oriented Programming, Systems, Languages & Applications • PLDI 2023: 44th ACM SIGPLAN Conf. on Programming Language Design and Implementation • ICFP 2022: 27th ACM SIGPLAN International Conference on Functional Programming •  DISC 2021: 35th International Symposium on DIStributed Computing • CPP 2021:  10th ACM SIGPLAN International Conference on Certified Programs and Proofs • VMCAI 2021: 22nd Conference on Verification, Model Checking, and Abstract Interpretation • APLAS 2020: 18th Asian Symposium on Programming Languages and Systems • PLDI 2020: 41st ACM SIGPLAN Conf. on Prog. Lang. Design and Impl. (External Programme Committee) • FLOPS 2020: 15th International Symposium on Functional and Logic Programming • ESOP 2020: 29th European Symposium on Programming • CPP 2020:  9th ACM SIGPLAN International Conference on Certified Programs and Proofs • PLDI 2019: 40th ACM SIGPLAN Conf. on Programming Language Design and Implementation • ECOOP 2019: 33rd European Conference on Object-Oriented Programming • Tokenomics 2019: International Conference on Blockchain Economics, Security and Protocols • POPL 2019: 46th ACM SIGPLAN Symposium on Principles of Programming Languages • APLAS 2018: 16th Asian Symposium on Programming Languages and Systems • ICFP 2018: 23rd ACM SIGPLAN International Conference on Functional Programming • APLAS 2017: 15th Asian Symposium on Programming Languages and Systems • Scala 2017: Scala Symposium 2017 • SAS 2017: 24th Static Analysis Symposium • POPL 2017: 44th ACM SIGPLAN Symposium on Principles of Programming Languages • TMPA 2017: 4th International Conference on Tools And Methods of Program Analysis • Scala 2016: Scala Symposium 2016 • ESOP 2016: 25th European Symposium on Programming • SEIM 2016: 1st Russian Conference on Software Engineering and Information Management • PPDP 2014: 16th International Symp. on Principles and Practice of Declarative Programming
PC Member for International Workshops
• FUNARCH 2024: The Second ACM SIGPLAN Workshop on Functional Software Architecture • PEPM 2023: ACM SIGPLAN 2023 Workshop on Partial Evaluation and Program Manipulation • FMBC 2021: 3rd Workshop on Formal Methods for Blockchains • PriSC 2021: Workshop on Principles of Secure Compilation 2021 • miniKanren 2020: miniKanren and Relational Programming Workshop 2020 • FMBC 2020: 2nd Workshop on Formal Methods for Blockchains • Coq 2019: The Coq Workshop 2019 • PEPM 2019: ACM SIGPLAN 2019 Workshop on Partial Evaluation and Program Manipulation • HOPE 2018: The 6th ACM SIGPLAN Workshop on Higher-Order Programming with Effects • WTSC 2018: 2nd Workshop on Trusted Smart Contracts • WTSC 2017: 1st Workshop on Trusted Smart Contracts • PEPM 2017: ACM SIGPLAN 2017 Workshop on Partial Evaluation and Program Manipulation • TAPAS 2016: The Seventh Workshop on Tools for Automatic Program Analysis • STOP 2015: International Workshop on Scripts to Programs • Scala 2014: The Fifth Annual Scala Workshop
Reviewing for Journals
•  ACM Computing Surveys (2019) •  Science of Computer Programming (SCP) (2019 × 2) •  Journal of Automated Reasoning (JAR) (2017) • ACM Transactions on Programming Languages and Systems (TOPLAS) (2014, 2015 × 2, 2016, 2017) • Philosophical Transactions of the Royal Society of London (2017), •  Journal of Functional Programming (JFP) (2015) •  Formal Aspects of Computing (2015).
Additional Conference and Workshop Refereeing
OOPSLA 2024, ICFP 2023, CAV 2023, POPL 2023, ICFP 2021, OOPSLA 2020, CONCUR 2020, S&P (Oakland) 2020, CONCUR 2018, ECOOP 2018, ISSTA 2018, ICALP 2018, PLDI 2018, S&P (Oakland) 2018, TYPES 2017 (Post-proceedings), PLDI 2017, TACAS 2017, ESOP 2017, ATVA 2016, CONCUR 2016, DISC 2015, ECOOP 2015, ESOP 2015, POPL 2015, GPCE 2014, ICFP 2014, CSF 2014, PROLE 2013, CC 2013, ESOP 2013, POPL 2013, CPP 2012, ECOOP 2012, NFM 2012, ESOP 2012, DSL 2011, IWACO 2011 , Coordination 2010, Coordination 2009.
Other Service
• Programming Languages Mentoring Workshop 2022 (PLMW 2022) @ POPL 2022, Speaker. Talk title: "Automatically Synthesising Programs that We Can Trust" •  Workshops Co-Chair for POPL 2022 •  Virtualization Committee member for PLDI 2021 • POPL 2021: •  Social Co-Chair (for the Asia-Pacific time band) • Student Research Competition, Selection Committee member • Contributor to the SIGPLAN PL Perspectives blog ( https://blog.sigplan.org ): • “Composition in Distributed Systems”, December 23, 2019. • "What Does It Mean for a Program Analysis to Be Sound?", August 7, 2019. • Programming Languages Mentoring Workshop 2019 (PLMW 2019) @ ICFP 2019, Speaker. Talk title: "Functional Programming is Everywhere" • Programming Languages Mentoring Workshop 2019 (PLMW 2019) @ POPL 2019, Speaker. Talk title: "Research Skills: How to Bootstrap a Research Project" •  Social Track at ICFP 2020, Panellist • PLDI 2019 , Student Research Competition, Selection Committee member • SPLASH 2017 Workshops, Workshop Program Committee member • ICFP 2017, September 2017, Oxford, UK. Student Research Competition Chair • ICFP 2016 , Student Research Competition, Selection Committee member • Programming Languages Mentoring Workshop at POPL 2016 , Panellist • ECOOP 2014, Artifact Evaluation Committee member
12    Appearances in Press
Online media
・ Scilla – A Formal Verification Oriented Contract Language Epicenter , video interview. 6 June 2018. https://epicenter.tv/episode/238/ • Security Vulnerabilities in Smart Contracts Schneier on Security. By Bruce Schneier, 6 March 2018. https://www.schneier.com/blog/archives/2018/03/security_vulner_13.html •  Ethereum's smart contracts are full of holes MIT Technology Review. By Mike Orcutt, 1 March 2018. https://www.technologyreview.com/s/610392/ethereums-smart-contracts-are-full-of-holes/ •  Millions of Dollars In Ethereum Are Vulnerable to Hackers Right Now Motherboard, Vice. By Jordan Pearson, 22 February 2018. https://goo.gl/Z68sbr