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.
Research Areas
Authored Publications
Sort By
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
