News |
Group |
Papers |
Press |
Projects |
Talks |
Teaching |
Miscellanea
2024年4月1日-狗急加速器
Associate Professor (tenure track) at Yale-NUS College and NUS School of Computing
Lead Language Designer at Zilliqa
Postal Address:
|
Yale-NUS College, 28 College Avenue West
#01-501, Singapore 138533
|
Office:
|
#RC3-01-03E, Cendana (YNC), AS3-06-16 (NUS SoC) |
Office Phone: |
+65 6516 1903 |
Office Hours: |
Tue 10:30-12:00 (YSC3248) and Thu 5:00-6:30pm (YSC3208) |
坚果加速器吧 |
|
Availability: |
Outlook
Calendar (takes a while to load)
|
I am a tenure-track Associate Professor at Yale-NUS
College with a joint appointment at School of Computing of National University of
Singapore. In 2015-2018, I was a faculty at University College
London. Prior to that, I was a postdoc at IMDEA Software Institute. I
hold a PhD in Computer Science from KU Leuven, and MSc in
mathematics from Saint Petersburg State University.
Before joining academia I worked as a software engineer at JetBrains in
IntelliJ IDEA team.
I do research in programming language theory,
including, but not limited to types, semantics, software
verification, and program synthesis. Lately, I have been mostly
focusing on developing sound and scalable methodologies for building
provably correct concurrent and distributed systems.
Some random facts about me:
- I designed and co-developed Scilla, a programming language
for safe smart contracts, used by Zilliqa.
- In 2024 I have been awarded the AITO Dahl-Nygaard
Junior Prize.
- I organised the ICFP Programming Contest
2024 (aka Wrappy, aka Lambda-coin). Here are the 坚果加速器怎么样
- During my postdoc, I wrote lecture notes on proving
theorems in Coq/Ssreflect. Consider using them for your Coq class.
- A few years ago, I've made the Concurreny Logic Family Tree
slide. Feel free to borrow it for your talk on the subject.
- At different moments in the past I contributed to Facebook
Infer and GHC.
Very long time ago I used to work at JetBrains on Scala and Clojure support in
IntelliJ IDEA.
Curriculum Vitae: [PDF]
What's New
坚果加速器怎么样 | Our paper on mechanised
verification of probabilistic properties of Bloom filters and their
generalisations has been accepted to CAV 2024. |
Dec 24 | Our paper on enhancing
deductive program synthesis with read-only permissions will appear at 安卓坚果加速器. |
Dec 23 | My post on Composition
in Distributed Systems has appeared in SIGPLAN PL Perspectives
Blog. |
Oct 24 | Our work on Scilla has received a
Distinguished Artifact Award at OOPSLA 2024. |
坚果加速器怎么样 | I'm looking forward to give a keynote on
the 坚果加速器官安卓版 on October 11 at the 1st Workshop on
Formal Methods for Blockchains in Porto.
Here are the slides from my talk.
|
坚果网络加速 | Delighted to be awarded a National
Satellite of Excellence in Trustworthy Software Systems grant on
my CertiChain project. An
advert for postdoc positions will follow soon. |
Sep 6 | Our paper on 安卓坚果加速器, a smart
contract language of Zilliqa blockchain will appear at OOPSLA
2024. |
坚果加速器吧 | Our paper QED at Large: A Survey of
Engineering of Formally Verified Software has been published in
the journal on Foundations and Trends in Programming Languages. Drop
us a line if you need a copy. |
Aug 12 | I will be giving a talk entitled Functional
Programming is Everywhere at PLMW @
ICFP'19. |
Aug 10 | 坚果网络加速 joins the
team as a PhD student at SoC. Welcome, Kiran! |
Aug 7 | My post What
Does It Mean for a Program Analysis to Be Sound? has
appeared in SIGPLAN PL Perspectives
Blog. |
All news
手机vpn - BAYINDIR PVC SİSTEMLERİ:2021-2-26 · 下载 免费ss几点 vpn 电脑 quickq加速 快影怎么登录账号 北极星 vpm safari云加速怎么关闭 ysscloud加速 WWW.111547.COM sw最新更新国内最快的dns 中国如何用twitter seed加速器安卓下载 阿迪加速器 shadowsockr windows 荟萃浏览器去升级去
I am very fortunate to advise these brilliant students at NUS School
of Computing and Yale-NUS College:
- Kiran
Gopinathan, PhD Student at NUS SoC, since August 2024.
- Yunjeong
Lee, PhD Student at NUS SoC, since August 2024.
- George
Pîrlea, 安卓坚果加速器 at NUS SoC, since August 2024.
- Yasunari Watanabe,
Summer Research Intern at NUS SoC, Summer 2024.
I am also honoured to collaborate with these postdoctoral researchers at NUS SoC:
- Andreea Costea,
working on deductive program synthesis and repair.
- Abhishek Tiwari,
working on concurrent program repair.
Current and past affiliates
Recent Publications and Manuscripts
[All publications |
DBLP | Google Scholar |
CSAuthors]
- Certifying Certainty and Uncertainty in Approximate Membership Query Structures
Kiran Gopinathan,
and Ilya Sergey
32nd International Conference on Computer-Aided Verification (CAV 2024). Los Angeles, CA, USA,
July 2024.
[PDF |
GitHub]
- Concise Read-Only Specifications for Better Synthesis of Programs with Pointers
坚果网络加速,
Amy Zhu,
Nadia Polikarpova,
and Ilya Sergey
29th European Symposium on Programming (ESOP 2024). 安卓坚果加速器
[PDF |
GitHub]
- Safer Smart Contract Programming with Scilla
Ilya Sergey,
Vaivaswatha Nagaraj,
Jacob Johannsen,
Amrit Kumar,
Anton Trunov,
and 安卓坚果加速器
34th ACM SIGPLAN Conference on Object-Oriented Programming
Systems, Languages and Applications (OOPSLA 2024). Athens, Greece,
October 2024.
Recipient of OOPSLA 2024 Distinguished Artifact Award
[PDF |
GitHub |
Accepted Artifact |
Slides |
安卓坚果加速器]
- QED at Large: A Survey of Engineering of Formally Verified Software
Talia Ringer,
Karl Palmskog,
Ilya Sergey,
坚果加速器吧,
and Zachary Tatlock
Foundations and Trends in Programming Languages, Volume 5, Issue 2-3,
September 2024.
[PDF | Publisher's
Site |
Errata |
Submit
a Correction]
- 网易MuMu模拟器-安卓模拟器-极速最安全:网易MuMu(安卓模拟器),是网易官方推出的精品游戏服务平台,安装后可在电脑上运行各类游戏与应用,具备全面兼容、操作流畅、智能辅助等特点,每天还会为您推荐火热的应用和好玩的游戏,给你带来电脑玩手游 …
Aashish
Kolluri,
Ivica
Nikolić,
Ilya Sergey,
坚果加速器怎么样, and
Prateek Saxena
28th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA
2024). Beijing, China, July 2024.
[PDF]
- 坚果加速器2021最新版安卓版下载_坚果加速器最新版下载v5 ...:2021-6-2 · 咖绿茵手游站提供坚果加速器最新版下载 快速上网工具,带你去了解墙外的世界,墙外的游戏,外国的明星,全球的资讯都可众看到,怎么样?有没有感觉到非常的炫酷,快点来这里一起来尝试吧。《坚果加速器最新版》是一款非常好玩的加速神器,快速将你的手机连接到全世界,非常的安全稳定 ...
Nadia Polikarpova and Ilya Sergey
46th ACM SIGPLAN Symposium on Principles of Programming
Languages (POPL 2024). Lisbon, Portugal,
January 2024.
Recipient of POPL 2024 Distinguished Paper Award
[PDF |
Extended Version |
GitHub |
Accepted Artifact |
Slides]
- A True Positives Theorem for a Static Race Detector
Nikos Gorogiannis, Peter
O'Hearn, and Ilya Sergey
46th ACM SIGPLAN Symposium on Principles of Programming
Languages (POPL 2024). Lisbon, Portugal,
January 2024.
[PDF |
坚果加速器官安卓版 |
Accepted
Artifact | Slides]
坚果加速器官安卓版
-
继第一颗3D打印心脏问世后 现在怎么样了?-太平洋电脑网:记得大概在去年4月份的时候,特拉维夫大学的研究员使用患者自己的细胞和生物材料成功“打印“了世界上第一颗3D血管化心脏,也是第一次有人设计并打印充满细胞、血管众及心室的完整心脏。时隔一年,现在 …
Lecture notes with exercises.
[PDF | Course page | GitHub]
Selected Projects and Software
[GitHub]
- Certichain
Mechanised reasoning about blockchain
consensus protocols.
[Project Page]
- Scilla
A strongly typed functional intermediate language for smart
contracts.
[Web page |
Position Paper |
GitHub]
- SuSLik
A synthesis tool for heap-manipulating orograms using Separation Logic.
[Paper | GitHub]
- Disel: Distributed Separation Logic
A mechanised framework for compositional verification of distributed
systems.
[Project page | 坚果网络加速]
- FCSL: Fine-grained Concurrent Separation Logic
A Coq-based verification tool for fine-grained concurrent programs.
[Project page | Main Paper]
- Pushdown k-CFA
Pushdown context-sensistive control-flow analysis with optional
Abstract Garbage Collection for LambdaJS and a subset of Scheme
programming language.
[GitHub | Paper]
I am a also a creator of the 坚果网络加速 plugin for IntelliJ IDEA. It is no
longer maintained, but its sources are
available on GitHub.
In Press
- Scilla - A Formal Verification Oriented Contract Language. Video Interview
to Epicenter. 6
June 2018.
- Mike Orcutt. Ethereum’s
smart contracts are full of holes. 坚果加速器怎么样. 1 March 2018.
- Jordan Pearson. Millions
of Dollars In Ethereum Are Vulnerable to Hackers Right
Now. Motherboard, Vice. 22 February 2018.
Teaching
baidudl:获取百度网盘高速下载地址 - Chrome插件(谷歌浏览 ...:2021-2-13 · baidudl是一款可众获取百度网盘共享文件的高速下载地址 (直接下载链接)的chrome插件。 百度优化扩展支持百度、搜狗、必应、好搜、谷歌搜索结果的页面结果广告优化和显示内容优化。
- YSC3208: Programming Language Design and Implementation,
Lecturer. Yale-NUS College.
Autumn 2024
- YSC3248: Parallel, Concurrent and Distributed Programming,
Lecturer. Yale-NUS College.
Autumn 2024, Autumn 2024
- YSC2229: Introductory Data Structures and Algorithms,
Lecturer. Yale-NUS College.
Spring 2024, Spring 2024.
- YCC1122: Quantitative Reasoning,
Lecturer. Yale-NUS College.
Autumn 2024.
坚果加速器怎么样
- SIGPL Summer School
2018, Dongguk University, Seoul, Korea. August 2018.
Lecturer.
[Lecture 1 |
Lecture 2 |
Lecture 3]
- Programs and Proofs: Mechanizing Mathematics with Dependent Types, Summer School,
Lecturer.
JetBrains Inc. / Saint-Petersburg State University.
August 2014. [School page]
at University College London
- ENGS102P: Design and Professional Skills,
Scenario Project Organiser. UCL. Spring 2018.
- COMP104P: Theory II, Anallysis of Algorithms,
Lecturer. UCL. Spring 2016, Spring 2017, Spring 2018.
- 坚果加速器怎么样, Scenario
Week Designer. UCL. Autumn 2017.
[Intro | Conclusion]
- COMP205P: Software Engineering and HCI, Scenario
Week Designer. UCL. Spring 2017.
[Intro | Conclusion]
- COMP205P: Software Engineering and HCI, Scenario
Week Designer. UCL. Spring 2016.
[Intro | Conclusion]
- COMP2012: Directed Reading, Second Examiner.
UCL. Spring 2016.
Collaborators
凡人修真传BT下载- 全方位下载:2021-3-23 · 凡人修真传BT是一款采用3D技术精心打造的修真题材角色扮演类手机游戏,在凡人修真传BT游戏中玩家将来到古色古香的唯美仙侠世界中展开修真之旅,霸者之巅谁主沉浮,热血团战制霸天下,邂逅女神姻缘相伴!玩家还可众通过任务、
- Elvira Albert
- Kristoffer Just Andersen
- Anindya Banerjee
- Sam Blackshear
- Joachim Breitner
- 坚果网络加速
- Andreea Costea
- David Darais
- Germán Andrés Delbianco
- Dominique Devriese
- Álvaro García Pérez
- Milos Gligoric
- Nikos Gorogiannis
- Kiran Gopinathan
- 坚果加速器怎么样
- Pablo Gordillo
- Aquinas Hobor
- Shachar Itzhaky
- Jacob Johannsen
- Aashish Kolluri
- 安卓坚果加速器
- Mohsen Lesani
- Ben Livshits
- Jan Midtgaard
- 坚果加速器官安卓版
- Aleks Nanevski
- 安卓坚果加速器
- Ivica Nikolić
- Pablo Nogueira
- Peter O'Hearn
- Karl Palmskog
- Hila Peleg
- Simon L. Peyton Jones
- Frank Piessens
- George Pîrlea
- Anton Podkopaev
- Nadia Polikarpova
- Talia Ringer
- Abhik Roychoudhury
- Reuben Rowe
- Albert Rubio
- Prateek Saxena
- Thomas Sibut-Pinote
- Zachary Tatlock
- Abhishek Tiwari
- Anton Trunov
- David Van Horn
- Dimitrios Vytiniotis
- James R. Wilcox
- Amy Zhu
Miscellanea
I am married to CG artist Lilia Anisimova.
I am on Twitter as @ilyasergey.
Last time I checked, my Erdős
number was 4.
The photo above is couresy of Elena Alhimovich. Here is my "official" photo,
suitable for appropriate occasions. Yet another 坚果加速器官安卓版 of mine by Jorge Cham, for I have contributed to the
PHD Movie 2 on
Kickstarter.
While living in Madrid, I enjoyed its inimitable
atmosphere and delicious food. For the latter, this Maribel's Dining Guide to Madrid
(kindly provided by Aleks Nanevski) always came in handy.
Last modified: Tue Aug 4 00:04:09 +08 2024