Mon 8 Jan 2018 10:30 - 11:00 at Museum A - Verifying Programs and Systems Chair(s): Natarajan Shankar

We would like to use the Coq proof assistant to mechanically verify properties of Haskell programs. To that end, we present a tool, named <tt>hs-to-coq</tt>, that translates total Haskell programs into Coq programs via a shallow embedding. We apply our tool in three case studies – a lawful <tt>Monad</tt> instance, “Hutton’s razor”, and an existing data structure library – and prove their correctness. These examples show that this approach is viable: both that <tt>hs-to-coq</tt> applies to existing Haskell code, and that the output it produces is amenable to verification.

Mon 8 Jan

CPP-2018
10:30 - 12:00: CPP 2018 - Verifying Programs and Systems at Museum A
Chair(s): Natarajan ShankarSRI International, USA
CPP-201810:30 - 11:00
Talk
Antal Spector-Zabusky, Joachim BreitnerUniversity of Pennsylvania, Christine RizkallahUniversity of Pennsylvania, USA, Stephanie WeirichUniversity of Pennsylvania, USA
DOI
CPP-201811:00 - 11:30
Talk
Damien RouhlingUniversity of Côte d'Azur, France
DOI
CPP-201811:30 - 12:00
Talk
Christian DoczkalCNRS, France, Joachim BardSaarland University, Germany
DOI