Travelled to:1 × Denmark
1 × Estonia
1 × France
1 × Germany
1 × Italy
1 × United Kingdom
4 × USA
Collaborated with:A.Nanevski D.Clarke G.A.Delbianco A.Banerjee Á.García-Pérez N.Gorogiannis P.W.O'Hearn Anindya Banerjee 0001 N.Polikarpova D.Devriese F.Piessens M.Might P.Nogueira D.Vytiniotis S.L.P.Jones J.R.Wilcox Z.Tatlock R.Ley-Wild C.Earl D.V.Horn A.Gotsman Y.Meshman S.Blackshear V.Nagaraj J.Johannsen Amrit Kumar 0001 Anton Trunov Ken Chan Guan Hao J.Midtgaard D.Darais
Talks about:program (5) concurr (5) type (4) abstract (3) interpret (2) structur (2) gradual (2) analysi (2) static (2) recurs (2)
Person: Ilya Sergey
DBLP: Sergey:Ilya
Contributed to:
2015
20152014
2014
2014201320132012
2012
20112018
2016
20172018201920182019Wrote 18 papers:
- ESOP-2015-SergeyNB #algorithm #concurrent #specification #verification
- Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity (IS, AN, AB), pp. 333–358.
- PLDI-2015-SergeyNB #concurrent #fine-grained #source code #verification
- Mechanized verification of fine-grained concurrent programs (IS, AN, AB), pp. 77–87.
- ESOP-2014-NanevskiLSD #communication #concurrent #fine-grained
- Communicating State Transition Systems for Fine-Grained Concurrent Resources (AN, RLW, IS, GAD), pp. 290–310.
- PEPM-2014-Garcia-PerezNS #λ-calculus
- Deriving interpretations of the gradually-typed λ calculus (ÁGP, PN, IS), pp. 157–168.
- POPL-2014-SergeyVJ #analysis #composition #higher-order #theory and practice
- Modular, higher-order cardinality analysis in theory and practice (IS, DV, SLPJ), pp. 335–348.
- PEPM-2013-DevrieseSCP #domain-specific language #recursion
- Fixing idioms: a recursion primitive for applicative DSLs (DD, IS, DC, FP), pp. 97–106.
- PLDI-2013-SergeyDMMDCP #monad
- Monadic abstract interpreters (IS, DD, MM, JM, DD, DC, FP), pp. 399–410.
- ESOP-2012-SergeyC
- Gradual Ownership Types (IS, DC), pp. 579–599.
- ICFP-2012-EarlSMH #analysis #automaton #higher-order #source code
- Introspective pushdown analysis of higher-order programs (CE, IS, MM, DVH), pp. 177–188.
- LDTA-2011-SergeyC #automaton #recursion #type checking
- From type checking by recursive descent to type checking with an abstract machine (IS, DC), p. 2.
- ESOP-2018-Garcia-PerezGMS
- Paxos Consensus, Deconstructed and Abstracted (ÁGP, AG, YM, IS), pp. 912–939.
- OOPSLA-2016-SergeyNBD #concurrent #correctness #hoare #specification
- Hoare-style specifications as correctness conditions for non-linearizable concurrent objects (IS, AN, AB0, GAD), pp. 92–110.
- ECOOP-2017-DelbiancoSNB #concurrent #data type
- Concurrent Data Structures Linked in Time (GAD, IS, AN, AB0), p. 30.
- OOPSLA-2018-BlackshearGOS #composition #concurrent #detection #named
- RacerD: compositional static race detection (SB, NG, PWO, IS), p. 28.
- OOPSLA-2019-SergeyNJ0TH #contract #programming
- Safer smart contract programming with Scilla (IS, VN, JJ, AK0, AT, KCGH), p. 30.
- POPL-2018-SergeyWT #distributed #programming #protocol #proving
- Programming and proving with distributed protocols (IS, JRW, ZT), p. 30.
- POPL-2019-GorogiannisOS #detection #theorem
- A true positives theorem for a static race detector (NG, PWO, IS), p. 29.
- POPL-2019-PolikarpovaS #source code #synthesis
- Structuring the synthesis of heap-manipulating programs (NP, IS), p. 30.