Zulip Chat Archive

Stream: general

Topic: mini demo type theory


view this post on Zulip Johan Commelin (Mar 09 2020 at 12:30):

I've lost a hyperlink... there is a paper + repo of a mini "demo" type theory. I couldn't find it via the search. Does this ring a bell with anyone?

view this post on Zulip Mario Carneiro (Mar 09 2020 at 12:36):

what do you mean?

view this post on Zulip Johan Commelin (Mar 09 2020 at 12:37):

Does anyone know which paper I'm talking about, and does someone have a link?

view this post on Zulip Johan Commelin (Mar 09 2020 at 12:38):

It was a sort of demo project. Minimalist implementation of a type checker.

view this post on Zulip Jannis Limperg (Mar 09 2020 at 12:38):

LamdaPi maybe? https://www.andres-loeh.de/LambdaPi/LambdaPi.pdf

view this post on Zulip Johan Commelin (Mar 09 2020 at 12:39):

Thanks. That looks good. It doesn't look familiar. But it's probably isomorphic to whatever I've seen before.


Last updated: May 09 2021 at 20:11 UTC