mini demo type theory

Stream: general

[Johan Commelin]

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]

what do you mean?

[Johan Commelin]

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

[Johan Commelin]

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

[Jannis Limperg]

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

[Johan Commelin]

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