And here the formalized proof in less than 150 lines of code (in Agda) for Brzoz... | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

evolveyourmind on March 7, 2023 | parent | context | favorite | on: Show HN: Regex Derivatives (Brzozowski Derivatives...

And here the formalized proof in less than 150 lines of code (in Agda) for Brzozowski Derivatives for regex matching (and additional regular languages theorems): https://github.com/desi-ivanov/agda-regexp-automata

c0nstantine on March 7, 2023 [–]

Thanks for sharing. I am not familiar with Agda. Will take a look. There is somewhat similar code in COQ: https://github.com/coq-community/regexp-Brzozowski

DonaldPShimoda on March 7, 2023 | [–]

Just a small FYI, but the language's name (for now) is Coq, not COQ.

Consider applying for YC's Winter 2027 batch! Applications are open till November 2.
Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact