Topic: mini demo type theory
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?
Mario Carneiro (Mar 09 2020 at 12:36):
what do you mean?
Johan Commelin (Mar 09 2020 at 12:37):
Does anyone know which paper I'm talking about, and does someone have a link?
Johan Commelin (Mar 09 2020 at 12:38):
It was a sort of demo project. Minimalist implementation of a type checker.
Jannis Limperg (Mar 09 2020 at 12:38):
LamdaPi maybe? https://www.andres-loeh.de/LambdaPi/LambdaPi.pdf
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