Ilya Sergey | |
---|---|
Born | Leningrad, USSR | June , 1986
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 |
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.
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.
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.
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.
Kathleen Shanahan Fisher is an American computer scientist who specializes in programming languages and their implementation.
David Bacon is an American computer programmer.
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.
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.
{{cite journal}}
: Cite journal requires |journal=
(help)