Publications

[DBLP | Google Scholar]

Journal articles

  1. Modular, Higher-Order Cardinality Analysis in Theory and Practice
    Ilya Sergey, Dimitrios Vytiniotis, Joachim Breitner, and Simon Peyton Jones
    An extended version of our
    POPL 2014 paper.
    Accepted for publication in Journal of Functional Programming, 2017. Cambridge University Press.
    [Accepted PDF]

  2. Pushdown Flow Analysis with Abstract Garbage Collection
    J. Ian Johnson, Ilya Sergey, Christopher Earl, Matthew Might and David Van Horn
    An extended version of our ICFP 2012 paper.
    Journal of Functional Programming, volume 24, issue 2-3, pages 218-283, May 2014. Cambridge University Press.
    [PDF | DOI]

  3. A correspondence between type checking via reduction and type checking via evaluation
    Ilya Sergey and Dave Clarke
    Information Processing Letters, volume 112, issue 1-2, pages 13-20, January 2012. Elsevier.
    [PDF | Code]

Proceedings articles

  1. Programming and Proving with Distributed Protocols
    Ilya Sergey, James R. Wilcox, and Zachary Tatlock
    Conditionally accepted to 45th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2018). Los Angeles, CA, USA, January 2018. ACM.
    [Draft PDF | Code]

  2. Concurrent Data Structures Linked in Time
    Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski and Anindya Banerjee
    31st European Conference on Object-Oriented Programming (ECOOP 2017), Barcelona, Spain, June 2017.
    [PDF | arXiv | Artifact]

  3. Programming Language Abstractions for Modularly Verified Distributed Systems
    James R. Wilcox, Ilya Sergey, and Zachary Tatlock
    The 2nd Summit oN Advances in Programming Languages (SNAPL 2017), Pacific Grove, CA, USA, May 2017.
    [PDF | Slides]

  4. A Concurrent Perspective on Smart Contracts
    Ilya Sergey and Aquinas Hobor
    1st Workshop on Trusted Smart Contracts, April 2017.
    [PDF | Slides]

  5. Hoare-style Specifications as Correctness Conditions for Non-linearizable Concurrent Objects
    Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee and Germán Andrés Delbianco
    31st ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2016). Amsterdam, The Netherlands, November 2016. ACM.
    [PDF | arXiv | Project page | Slides | Video]

  6. Experience Report: Growing and Shrinking Polygons for Random Testing of Computational Geometry Algorithms
    Ilya Sergey
    21st ACM SIGPLAN International Conference on Functional Programming (ICFP 2016). Nara, Japan, September 2016. ACM.
    [PDF | GitHub | Slides | Video]

  7. Mechanized Verification of Fine-grained Concurrent Programs
    Ilya Sergey, Aleksandar Nanevski and Anindya Banerjee
    36th ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2015). Portland, OR, USA, June 2015. ACM.
    [PDF | Coq sources | Project page | Video Abstract | Slides]

  8. Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity
    Ilya Sergey, Aleksandar Nanevski and Anindya Banerjee
    24th European Symposium on Programming (ESOP 2015). London, UK, April 2015. Springer.
    [PDF | Extended version | arXiv | Project page | Slides]

  9. Communicating State Transition Systems for Fine-Grained Concurrent Resources
    Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey and Germán Andrés Delbianco
    23rd European Symposium on Programming (ESOP 2014). Grenoble, France, April 2014. Springer.
    [PDF | Extended version | Coq scripts | Project page | Slides]

  10. Modular, Higher-Order Cardinality Analysis in Theory and Practice ACM DL Author-ize service
    Ilya Sergey, Dimitrios Vytiniotis and Simon Peyton Jones
    41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2014). San Diego, CA, USA, January 2014. ACM.
    [
    PDF | Extended version | Slides]

  11. Deriving Interpretations of the Gradually-Typed Lambda Calculus ACM DL Author-ize service
    Álvaro García Pérez, Pablo Nogueira and Ilya Sergey
    ACM SIGPLAN 2014 Workshop on Partial Evaluation and Program Manipulation (PEPM 2014). San Diego, CA, USA, January 2014. ACM.
    [PDF]

  12. Monadic Abstract Interpreters ACM DL Author-ize service
    Ilya Sergey, Dominique Devriese, Matthew Might, Jan Midtgaard, David Darais, Dave Clarke and Frank Piessens
    34th ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2013). Seattle, WA, USA, June 2013. ACM.
    [PDF | Slides | Code]

  13. Fixing Idioms: A recursion primitive for applicative DSLs ACM DL Author-ize service
    Dominique Devriese, Ilya Sergey, Dave Clarke and Frank Piessens
    ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation (PEPM 2013). Rome, Italy, January 2013. ACM.
    [PDF | Slides]

  14. Introspective Pushdown Analysis of Higher-Order Programs ACM DL Author-ize service
    Christopher Earl, Ilya Sergey, Matthew Might and David Van Horn
    17th ACM SIGPLAN International Conference on Functional Programming (ICFP 2012). Copenhagen, Denmark, September 2012. ACM.
    [PDF | Slides | Video]

  15. Calculating Graph Algorithms for Dominance and Shortest Path
    Ilya Sergey, Jan Midtgaard and Dave Clarke
    11th International Conference on Mathematics of Program Construction (MPC 2012). Madrid, Spain, June 2012. Springer.
    [PDF | Slides]

  16. Gradual Ownership Types
    Ilya Sergey and Dave Clarke
    21st European Symposium on Programming (ESOP 2012). Tallinn, Estonia, April 2012. Springer.
    [PDF | Slides | Prototype]

  17. From type checking by recursive descent to type checking with an abstract machine ACM DL Author-ize service
    Ilya Sergey and Dave Clarke
    11th Workshop on Language Descriptions, Tools and Applications (LDTA 2011). Saarbrücken, Germany, March 2011. ACM.
    [PDF | Slides | Code]

  18. A semantics for context-oriented programming with layers ACM DL Author-ize service
    Dave Clarke and Ilya Sergey
    International Workshop on Context-Oriented Programming (COP 2009). Genova, Italy, June 2009. ACM
    [PDF | Slides]

Book chapters

  1. Ownership Types: A Survey
    Dave Clarke, Johan Östlund, Ilya Sergey and Tobias Wrigstad
    In Aliasing in Object-Oriented Programming: Types, Analysis and Verification, edited by Dave Clarke et al., volume 7850 of LNCS, pages 18-64, 2013. Springer-Verlag.
    [PDF]

Lecture notes

Theses

Other manuscripts

  1. Operational Aspects of C/C++ Concurrency
    Anton Podkopaev, Ilya Sergey and Aleksandar Nanevski
    Unpublished draft
    [Code | Draft]

  2. Introducing Functional Programmers to Interactive Theorem Proving and Program Verification
    Ilya Sergey and Aleksandar Nanevski
    Teaching Experience Report
    [PDF]

  3. Calculating Graph Algorithms by Abstract Interpretation
    Ilya Sergey, Jan Midtgaard and Dave Clarke
    An extended version of our MPC 2012 paper.
    [PDF]

  4. Implementation of Gradual Ownership Types for Java using Attribute Grammars (in Russian)
    Ilya Sergey
    Software Engineering, issue 6, pages 49-79, Saint Petersburg State University publishing, 2011.
    [PDF]

  5. Dominance Analysis via Ownership Types and Abstract Interpretation
    Ilya Sergey, Jan Midtgaard and Dave Clarke
    CW Reports, volume CW615. Department of Computer Sciences, KU Leuven. December 2011.
    [PDF | Prototype]

  6. Towards Gradual Ownership Types
    Ilya Sergey and Dave Clarke
    International Workshop on Aliasing, Confinement and Ownership (IWACO 2011). Lancaster, UK, July 2011.

  7. Scripting an IDE for EDSL awareness
    Ilya Sergey, Peter Gromov and Dave Clarke
    CW Reports, volume CW608. Department of Computer Sciences, KU Leuven. July 2011.
    [PDF]

  8. Automatic refactorings for Scala programs
    Ilya Sergey, Dave Clarke and Alexander Podkhalyuzin
    The First Scala Workshop -- Scala Days 2010. Lausanne, Switzerland, April 2010.
    [PDF | Video]

  9. Implementation of JVM-based languages support in IntelliJ IDEA
    Ilya Sergey
    International Workshop Workshop on Multiparadigm Programming with Object-Oriented Languages (MPOOL 2008). Paphos, Cyprus, July 2008.
    [PDF]

Main page