ICFP 2022
Sun 11 - Fri 16 September 2022 Ljubljana, Slovenia
Thu 15 Sep 2022 11:00 - 11:30 at Kosovel - Verification Chair(s): Wouter Swierstra

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 Sep

Displayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change

11:00 - 12:30
VerificationHaskell at Kosovel
Chair(s): Wouter Swierstra Utrecht University, Netherlands
11:00
30m
Talk
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
30m
Talk
How to Safely Use Extensionality in Liquid Haskell
Haskell
Niki Vazou IMDEA Software Institute, Michael Greenberg Stevens Institute of Technology
12:00
30m
Talk
Liquid Proof Macros
Haskell
Henry Blanchette , Niki Vazou IMDEA Software Institute, Leonidas Lampropoulos University of Maryland, College Park