[Agda-dev] Fwd: Calling all type system implementors

[Jesper Cockx]

Hi Agda developers,

Richard Eisenberg recently started a new mailing list aimed at implementers
of (dependent) type systems (see below). I think it is a great idea to
collaborate more between different languages, so please consider joining
the list!

-- Jesper

---------- Forwarded message ---------
From: Richard Eisenberg <rae at cs.brynmawr.edu>
Date: Fri, Oct 12, 2018 at 5:21 AM
Subject: Calling all type system implementors
To: Richard Eisenberg <rae at cs.brynmawr.edu>


Hi colleagues,

Recently back from ICFP, I want the collaboration and sharing of knowledge
to continue. Whenever I'm in the presence of others working on similar
problems to the ones I face in GHC, I'm inspired by the work you do and
enjoy finding the ways in which the problems we have are similar. So, I
decided to set up a mailing list where we can share knowledge, ask
questions of each other, and collaborate in general.

My goal here is to bring together the type system grease monkeys of the
world: we who both design these complex systems and implement them. I'm
hoping that the list will contain discussions of, say, implementation
tricks in higher-order unification, or thoughts about kind inference of
datatype declarations parameterized by telescopes with internal dependency,
or even syntactic choices around irrelevant function arguments. We are an
odd, select bunch who share our passion for these fun problems, and we have
much to learn from each other.

This email is going out to members of the communities from the following
languages: GHC, Ocaml, Idris, Agda, Coq, Scala, and Rust. I know GHC fairly
well, but not so much the others. Please forward to the individuals in your
communities who know the most about your respective type systems and their
implementations -- in some cases, I got your names solely by scrolling
through recent commit histories. Also, please feel free to forward to other
language communities. I'm not trying to exclude anyone!

If you're interested in joining the list, you may do so here:
https://lists.cs.brynmawr.edu/listinfo/type-sys-impl

Thanks!
Richard

-=-=-=-=-=-=-=-=-=-=-
Richard A. Eisenberg, PhD
Asst. Prof. of Computer Science
Bryn Mawr College
Bryn Mawr, PA, USA
cs.brynmawr.edu/~rae
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda-dev/attachments/20181013/1a31cac4/attachment.html>