Jump to Content
Nikolaos Papaspyrou

Nikolaos Papaspyrou

Software Engineer at Google, in Chrome/V8 (MUC). Professor (on leave) at the School of Electrical and Computer Engineering of the National Technical University of Athens and a member of the Software Engineering Laboratory. I am interested in the theory and implementation of programming languages: semantics, type systems, compilers, static analysis, formal verification.
Authored Publications
Google Publications
Other Publications
Sort By
  • Title
  • Title, descending
  • Year
  • Year, descending
    Coinduction Inductively: Mechanizing Coinductive Proofs in Liquid Haskell
    Lykoyrgos Mastorou
    Niki Vazou
    Proceedings of the 15th ACM SIGPLAN International Haskell Symposium, ACM Press, New York, NY, USA (2022), pp. 1-12
    Preview abstract Liquid Haskell is an inductive verifier that cannot reason about codata. In this work we present two alternative approaches, namely indexed and constructive coinduction, to consistently encode coinductive proofs in Liquid Haskell. The intuition is that indices can be used to enforce the base case in the setting of classical logic and the guardedness check in the constructive proofs. We use our encodings to machine check 10 coinductive proofs, about unary and binary predicates on infinite streams and lists, showcasing how an inductive verifier can be used to check coinductive properties of Haskell code. View details
    No Results Found