ICFP 2022 (series) / Haskell 2022 (series) / Haskell 2022 /
Coinduction Inductively: Mechanizing Coinductive Proofs in Liquid Haskell
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.
Thu 15 SepDisplayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change
Thu 15 Sep
Displayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change
11:00 - 12:30 | |||
11:00 30mTalk | Coinduction Inductively: Mechanizing Coinductive Proofs in Liquid Haskell Haskell Lykourgos Mastorou National Technical University of Athens, Nikolaos Papaspyrou National Technical University of Athens, Niki Vazou IMDEA Software Institute | ||
11:30 30mTalk | How to Safely Use Extensionality in Liquid Haskell Haskell | ||
12:00 30mTalk | Liquid Proof Macros Haskell Henry Blanchette , Niki Vazou IMDEA Software Institute, Leonidas Lampropoulos University of Maryland, College Park |