On Fri, Jan 22, 2021 at 12:56 AM Hendrik Boom <hend...@topoi.pooq.com> wrote:
> [...] > > You might also want to look at the implementations of category theory in Agda. > Agda is a language which unifies execution and correctness proof to some > extent. > > Not that you want to implement catagory theory, but category theory is a > form of algebra, and you may find some useful ideas about syntax and > semantics there. > > I attended an online seminar about this recently, but I haven't been > able to find the details again. The following links seem to refer to the > same project. (I found them looking for > category theory in agda Thanks Hendrik -- I had forgotten that Agda (and Idris, Coq, Lean) are also good sources of inspiration in this general area. Stu -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/CAG%2BkMrGTrbQuoFuYq%2BGWQKch0VZukQyuc6ngR0jhAwsxvidXVw%40mail.gmail.com.
