Ilya Sergey

Last updated
Ilya Sergey
Born(1986-06-00)June , 1986
Leningrad, USSR
Alma mater St Petersburg State University (MSc)
KU Leuven (PhD)
Awards 2019 Dahl-Nygaard Junior Prize
Scientific career
Fields Computer science
Programming languages
Formal methods
Institutions University College London
National University of Singapore
Yale-NUS College
Thesis Operational Aspects of Type Systems  (2012)
Website ilyasergey.net

Ilya Sergey (born 1986) is a Russian computer scientist and an Associate Professor at the School of Computing at the National University of Singapore, [1] where he leads the Verified Systems Engineering lab. [2] Sergey does research in programming language design and implementation, software verification, distributed systems, program synthesis, and program repair. He is known for designing the Scilla programming language for smart contracts. [3] He is the author of the free online book Programs and Proofs: Mechanizing Mathematics with Dependent Types, Lecture notes with exercises, which introduce the basic concepts of mechanized reasoning and interactive theorem proving using Coq.

Contents

Sergey holds a joint appointment at Yale-NUS College [4] and is a lead language designer at Zilliqa. [5] He received his MSc in 2008 at Saint Petersburg State University and his PhD in 2012 at KU Leuven. Before joining NUS, he was a postdoctoral researcher at IMDEA Software Institute and on the faculty of University College London. Prior to starting an academic career, he worked as a software developer at JetBrains.

Awards and honors

Related Research Articles

In computer science, abstract interpretation is a theory of sound approximation of the semantics of computer programs, based on monotonic functions over ordered sets, especially lattices. It can be viewed as a partial execution of a computer program which gains information about its semantics without performing all the calculations.

Brent Hailpern is a computer scientist retired from IBM Research. His research work focused on programming languages, software engineering, and concurrency.

The annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) is an academic conference in the field of computer science, with focus on fundamental principles in the design, definition, analysis, and implementation of programming languages, programming systems, and programming interfaces. The venue is jointly sponsored by two Special Interest Groups of the Association for Computing Machinery: SIGPLAN and SIGACT.

Dexter Campbell Kozen is an American theoretical computer scientist. He is Joseph Newton Pew, Jr. Professor in Engineering at Cornell University. He received his B.A. from Dartmouth College in 1974 and his PhD in computer science in 1977 from Cornell University, where he was advised by Juris Hartmanis. He advised numerous Ph.D. students.

<span class="mw-page-title-main">Incremental computing</span> Software feature

Incremental computing, also known as incremental computation, is a software feature which, whenever a piece of data changes, attempts to save time by only recomputing those outputs which depend on the changed data. When incremental computing is successful, it can be significantly faster than computing new outputs naively. For example, a spreadsheet software package might use incremental computation in its recalculation feature, to update only those cells containing formulas which depend on the changed cells.

In type theory, a refinement type is a type endowed with a predicate which is assumed to hold for any element of the refined type. Refinement types can express preconditions when used as function arguments or postconditions when used as return types: for instance, the type of a function which accepts natural numbers and returns natural numbers greater than 5 may be written as . Refinement types are thus related to behavioral subtyping.

In computer science, region-based memory management is a type of memory management in which each allocated object is assigned to a region. A region, also called a zone, arena, area, or memory context, is a collection of allocated objects that can be efficiently reallocated or deallocated all at once. Like stack allocation, regions facilitate allocation and deallocation of memory with low overhead; but they are more flexible, allowing objects to live longer than the stack frame in which they were allocated. In typical implementations, all objects in a region are allocated in a single contiguous range of memory addresses, similarly to how stack frames are typically allocated.

Bernhard Steffen is a German computer scientist and professor at the TU Dortmund University, Germany. His research focuses on various facets of formal methods ranging from program analysis and verification, to workflow synthesis, to test-based modeling, and machine learning.

Susan Beth Horwitz was an American computer scientist noted for her research on programming languages and software engineering, and in particular on program slicing and dataflow-analysis. She had several best paper and an impact paper award mentioned below under awards.

<span class="mw-page-title-main">Kathleen Fisher</span> American computer scientist

Kathleen Shanahan Fisher is an American computer scientist who specializes in programming languages and their implementation.

David Bacon is an American computer programmer.

<span class="mw-page-title-main">Grigore Roșu</span> Computer science professor

Grigore Roșu is a computer science professor at the University of Illinois at Urbana-Champaign and a researcher in the Information Trust Institute. He is known for his contributions in runtime verification, the K framework, matching logic, and automated coinduction.

Runtime predictive analysis is a runtime verification technique in computer science for detecting property violations in program executions inferred from an observed execution. An important class of predictive analysis methods has been developed for detecting concurrency errors in concurrent programs, where a runtime monitor is used to predict errors which did not happen in the observed run, but can happen in an alternative execution of the same program. The predictive capability comes from the fact that the analysis is performed on an abstract model extracted online from the observed execution, which admits a class of executions beyond the observed one.

<span class="mw-page-title-main">Yannis Smaragdakis</span> American computer scientist

Yannis Smaragdakis is a Greek-American software engineer, computer programmer, and researcher. He is a professor in the Department of Informatics and Telecommunications at the University of Athens. He is the author of more than 130 research articles on a variety of topics, including program analysis, declarative languages, program generators, language design, and concurrency. He is best known for work in program generation and program analysis and the Doop framework.

Martin Vechev is a professor at the Department of Computer Science at ETH Zurich working in the fields of programming languages, machine learning, and security. He leads the Secure, Reliable, and Intelligent Systems Lab (SRI), part of the Department of Computer Science. He is known for his pioneering works in machine learning for code (BigCode), where he introduced statistical programming engines trained on large codebases, reliable and trustworthy artificial intelligence, where he introduced abstract interpretation methods for reasoning about deep neural networks to enable the verification of large machine learning models, and quantum programming, introducing the first high-level programming language and system Silq.

In computer science, choreographic programming is a programming paradigm where programs are compositions of interactions among multiple concurrent participants.

Todd Millstein is an American computer scientist. He is Professor of Computer Science and Chair of the Department at the UCLA Henry Samueli School of Engineering and Applied Science.

Soufflé is an open source parallel logic programming language, influenced by Datalog. Soufflé includes both an interpreter and a compiler that targets parallel C++. Soufflé has been used to build static analyzers, disassemblers, and tools for binary reverse engineering. Soufflé is considered by academic researchers to be high-performance and "state of the art," and is often used in benchmarks in academic papers.

References

  1. "NUS Computing Faculty Photo Directory" . Retrieved 2022-10-05.
  2. "Verse: Verified Systems Engineering@US" . Retrieved 2022-10-05.
  3. 1 2 Sergey, Ilya; Nagaraj, Vaivaswatha; Johannsen, Jacob; Kumar, Amrit; Trunov, Anton; Hao, Ken Chan Guan (October 2019). Stephen N. Freund; Eran Yahav (eds.). "Safer smart contract programming with Scilla". Proc. ACM Program. Lang. Proceedings of the ACM on Programming Languages (PACMPL). Association for Computing Machinery. 3 (OOPSLA): 1–30. doi: 10.1145/3360611 . S2CID   203577198.
  4. "Yale NUS College: Ilya Sergey" . Retrieved 2022-10-05.
  5. "Zilliqa: Our Team" . Retrieved 2022-10-05.
  6. "OOPSLA Artifacts" . Retrieved 2022-10-06.
  7. The announcement of the four artifacts chosen as distinguished appear two-thirds of the way down on this web page [6]
  8. Sergey, Ilya; Vaivaswatha Nagaraj; Johannsen, Jacob; Kumar, Amrit; Trunov, Anton; Hao, Ken Chan Guan (2019). "ilyasergey/scilla-benchmarks: OOPSLA 2019 Artefact". doi:10.5281/zenodo.3368504 . Retrieved 2022-10-07.{{cite journal}}: Cite journal requires |journal= (help)
  9. "POPL 2019 Distinguished Paper" . Retrieved 2022-10-06.
  10. Polikarpova, Nadia; Sergey, Ilya (January 2019). "Structuring the synthesis of heap-manipulating programs". Proc. ACM Program. Lang. Proceedings of the ACM on Programming Languages. ACM. 3 (POPL): 1–30. doi: 10.1145/3290385 . S2CID   49867437.
  11. "Distinguished Papers" . Retrieved 2022-10-06.
  12. Itzhaky, Shachar; Peleg, Hila; Polikarpova, Nadia; Rowe, Reuben N S; Sergey, Ilya (June 2021). "Cyclic program synthesis". PLDI 2021: Proceedings of the 42nd ACM SIGPLAN Conference on Programming Language Design and Implementation. Vol. 2. ACM. pp. 994–969. doi: 10.1145/3453483.3454087 .
  13. "Annual Research Recognition Awards celebrate Yale-NUS faculty achievements" . Retrieved 2022-10-07.