type: long talk
audience: intermediate
category: type-level, verification, Idris
Summary
A couple of months ago I started a small endeavor into Idris by working (partially) through Edwan Brady's introduction book Type Driven Development and implemention Specris. But in the I wrote Haskell like Idris code, which means I didn't really leveraged the powerful proof system underlying Idris.
It could be very interesting if someone with experience in writing proofs in Idris (or Coq, Agda) could give us an introduction into the topi. Maybe we could continue that topic with a workshop.
type: long talk
audience: intermediate
category: type-level, verification, Idris
Summary
A couple of months ago I started a small endeavor into Idris by working (partially) through Edwan Brady's introduction book Type Driven Development and implemention Specris. But in the I wrote Haskell like Idris code, which means I didn't really leveraged the powerful proof system underlying Idris.
It could be very interesting if someone with experience in writing proofs in Idris (or Coq, Agda) could give us an introduction into the topi. Maybe we could continue that topic with a workshop.