4
$\begingroup$

I am trying to find a minimal implementation of dependent type theory that supports

  • Pi Types (obviously)
  • Modules containing records
  • Inductive data types
  • Universe Hierarchy
  • A notion of equality
  • Termination checker
  • Type Inference and Resolution

I am aware of implementations based on:

Löh, A., McBride, C., & Swierstra, W. (2010). A tutorial implementation of a dependently typed lambda calculus. Fundamenta informaticae, 102(2), 177-207.

But they do not support everything in the list above.

Something even smaller than mini-Agda would be helpful.

$\endgroup$
  • 2
    $\begingroup$ I'm voting to close this question as off-topic because it is a request for softwre, rather than a question in theoretical computer science. $\endgroup$ – Andrej Bauer Dec 5 '19 at 16:57
  • 2
    $\begingroup$ Also, your wish list is kind of optimistic, as you're asking for a fairly complex type theory. I'm not sure it can be much smaller than some fragment of Agda. It would help if you explained what you need this for. $\endgroup$ – Andrej Bauer Dec 5 '19 at 16:59
  • 1
    $\begingroup$ @AndrejBauer Hello, I apologize if my question is off-topic. Do you have a recommendation of another venue for posting it? $\endgroup$ – Yasmine Shaorda Dec 5 '19 at 17:52
  • 1
    $\begingroup$ I am implementing a DSL that manipulates axiomatic theories (presented as dependent record types). I want an implementation of DTT to typecheck my DSL constructs. I do not want to worry about all of the details of a full-scale theorem prover, nor commit to any of them. $\endgroup$ – Yasmine Shaorda Dec 5 '19 at 17:58
  • 2
    $\begingroup$ So why do you need a termination checker? For representation of syntax of axiomatic theories some very simple inductive types ought to suffice. And the universe hierarchy, what's that for? In any case, I'd recommend asking on the Types mailing list. $\endgroup$ – Andrej Bauer Dec 5 '19 at 21:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.