from Hacker News

Verified Functional Programming in Agda

by TheAsprngHacker on 4/5/20, 3:59 AM with 10 comments

• by lightgreen on 4/5/20, 5:47 AM

  One thing I love about Agda is that it translates to Idris (which is much more friendly to a regular programmer) almost mechanically.

  Once I needed to write a proof of permutation transitivity in Idris. I’m not smart enough to write it myself, but I found a proof in Agda and translated it to Idris in 20 minutes. https://github.com/stepancheg/idris-sort/blob/master/PermHar...

• by JadeNB on 4/5/20, 5:55 PM

  Reminder that all ACM Digital Library resources, including books, are free until June 30.

  https://www.acm.org/articles/bulletins/2020/march/dl-access-...

• by thekhatribharat on 4/5/20, 7:01 AM

  I put a related question on Computer Science Stack Exchange a week ago. Linking it here in the hopes that HN users roll-calling here will shed some light.

  Ref: https://cs.stackexchange.com/questions/122066/does-the-under...

• by evolveyourmind on 4/5/20, 7:43 AM

  How can I prove dfs graph termination in Agda? I tried passing "visited" subset but nothing

• by FrankyHollywood on 4/5/20, 1:20 PM

  thx a lot, found some other interesting books along the way!

  https://dl.acm.org/acmbooks