On Fri, Jan 22, 2021 at 12:56 AM Hendrik Boom <[email protected]> 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/CAG%2BkMrGTrbQuoFuYq%2BGWQKch0VZukQyuc6ngR0jhAwsxvidXVw%40mail.gmail.com.
