Ilya Sergey
@ilyasergey@types.pl
mastodon
4.6.0-alpha.5+glitch
Associate Prof at NUS School of Computing. PL, proofs, systems, pictures of corgi.
https://ilyasergey.net
0
Followers
0
Following
Joined November 15, 2022
Posts
Ilya Sergey
@ilyasergey@types.pl
Associate Prof at NUS School of Computing. PL, proofs, systems, pictures of corgi. https://ilyasergey.net
types.pl
Ilya Sergey
@ilyasergey@types.pl
Associate Prof at NUS School of Computing. PL, proofs, systems, pictures of corgi. https://ilyasergey.net
types.pl
@ilyasergey@types.pl
·
Aug 13, 2025
@markusde @krismicinski @kha yes, we are working on this right now, taking a lot of inspiration from Pulse and recent Iris-related works. Stay tuned. :)
2
0
0
Ilya Sergey
@ilyasergey@types.pl
Associate Prof at NUS School of Computing. PL, proofs, systems, pictures of corgi. https://ilyasergey.net
types.pl
Ilya Sergey
@ilyasergey@types.pl
Associate Prof at NUS School of Computing. PL, proofs, systems, pictures of corgi. https://ilyasergey.net
types.pl
@ilyasergey@types.pl
·
Aug 13, 2025
@krismicinski send me an email.
0
0
0
Ilya Sergey
@ilyasergey@types.pl
Associate Prof at NUS School of Computing. PL, proofs, systems, pictures of corgi. https://ilyasergey.net
types.pl
Ilya Sergey
@ilyasergey@types.pl
Associate Prof at NUS School of Computing. PL, proofs, systems, pictures of corgi. https://ilyasergey.net
types.pl
@ilyasergey@types.pl
·
Aug 13, 2025
@krismicinski @kha @markusde in a way, yes, but not in the full Iris-style generality. We think of Lean as an IR to embed sound domain-specific verifiers with a good amount of proof automation and lightweight validation.
4
1
0
Ilya Sergey
@ilyasergey@types.pl
Associate Prof at NUS School of Computing. PL, proofs, systems, pictures of corgi. https://ilyasergey.net
types.pl
Ilya Sergey
@ilyasergey@types.pl
Associate Prof at NUS School of Computing. PL, proofs, systems, pictures of corgi. https://ilyasergey.net
types.pl
@ilyasergey@types.pl
·
Sep 22, 2024
@koronkebitch @wilbowma @atsuzaki @secretasianman the ICFP’25 announcent, for extra motivation:
https://www.dropbox.com/scl/fi/2su0bt0chcpbqpqhspaoz/ICFP25-announcement.pdf?rlkey=yghbloixz6j777y6c02rt53vi&dl=0
https://www.dropbox.com/scl/fi/2su0bt0chcpbqpqhspaoz/ICFP25-announcement.pdf?rlkey=yghbloixz6j777y6c02rt53vi&dl=0
5
1
0
Ilya Sergey
@ilyasergey@types.pl
Associate Prof at NUS School of Computing. PL, proofs, systems, pictures of corgi. https://ilyasergey.net
types.pl
Ilya Sergey
@ilyasergey@types.pl
Associate Prof at NUS School of Computing. PL, proofs, systems, pictures of corgi. https://ilyasergey.net
types.pl
@ilyasergey@types.pl
·
Sep 22, 2024
3
1
0
Ilya Sergey
@ilyasergey@types.pl
Associate Prof at NUS School of Computing. PL, proofs, systems, pictures of corgi. https://ilyasergey.net
types.pl
Ilya Sergey
@ilyasergey@types.pl
Associate Prof at NUS School of Computing. PL, proofs, systems, pictures of corgi. https://ilyasergey.net
types.pl
@ilyasergey@types.pl
·
Sep 19, 2024
@krismicinski on those days I (1) don’t check email until late afternoon and (2) work from a coffee shop.
0
0
0
Ilya Sergey
@ilyasergey@types.pl
Associate Prof at NUS School of Computing. PL, proofs, systems, pictures of corgi. https://ilyasergey.net
types.pl
Ilya Sergey
@ilyasergey@types.pl
Associate Prof at NUS School of Computing. PL, proofs, systems, pictures of corgi. https://ilyasergey.net
types.pl
@ilyasergey@types.pl
·
Sep 19, 2024
@krismicinski have you considered making one day (or two, or three) a week fully clear from teaching, meeting, and admin, focusing it solely on research?
0
0
0
Ilya Sergey
@ilyasergey@types.pl
Associate Prof at NUS School of Computing. PL, proofs, systems, pictures of corgi. https://ilyasergey.net
types.pl
Ilya Sergey
@ilyasergey@types.pl
Associate Prof at NUS School of Computing. PL, proofs, systems, pictures of corgi. https://ilyasergey.net
types.pl
@ilyasergey@types.pl
·
Sep 14, 2024
@wicko3@mastodonapp.uk it is interesting to observe how more and more verification researchers realise that working on testing (and fuzz-testing specifically) makes it (a) easier to get industry interest by finding bugs that matter, (b) attract students, and (c) increase your publication rate.
0
0
0
Ilya Sergey
@ilyasergey@types.pl
Associate Prof at NUS School of Computing. PL, proofs, systems, pictures of corgi. https://ilyasergey.net
types.pl
Ilya Sergey
@ilyasergey@types.pl
Associate Prof at NUS School of Computing. PL, proofs, systems, pictures of corgi. https://ilyasergey.net
types.pl
@ilyasergey@types.pl
·
Sep 11, 2024
@krismicinski thank you Kris, you are very kind!
These notes show how much more energy I used to have while on tenure track.
These notes show how much more energy I used to have while on tenure track.
0
0
0