<p>I am trying to find a minimal implementation of dependent type theory that supports </p>

<ul>
<li>Pi Types (obviously) </li>
<li>Modules containing records</li>
<li>Inductive data types</li>
<li>Universe Hierarchy </li>
<li>A notion of equality</li>
<li>Termination checker</li>
<li>Type Inference and Resolution</li>
</ul>

<p>I am aware of implementations based on: </p>

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

<p>But they do not support everything in the list above. </p>

<p>Something even smaller than mini-Agda would be helpful. </p>

CC BY-SA 4.0
2019-12-05T16:57:42.390Z
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.
Andrej Bauer
CC BY-SA 4.0
2019-12-05T16:59:10.493Z
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.
Andrej Bauer
CC BY-SA 4.0
2019-12-05T17:52:11.897Z
@AndrejBauer Hello, I apologize if my question is off-topic. Do you have a recommendation of another venue for posting it?
Yasmine Shaorda
CC BY-SA 4.0
2019-12-05T17:58:35.983Z
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.
Yasmine Shaorda
CC BY-SA 4.0
2019-12-05T21:51:28.640Z
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](https://lists.seas.upenn.edu/mailman/listinfo/types-list).
Andrej Bauer
CC BY-SA 4.0
2019-12-05T21:56:06.450Z
And maybe some of the work of William Bowman could be relevant, see his [Gorwing a proof assistant](https://www.williamjbowman.com/resources/cur.pdf).
Andrej Bauer
CC BY-SA 4.0
2019-12-07T19:49:03.997Z
I think the most minimal you can get is Coq.
xrq
<type-theory><dependent-type>
Implementations of Dependent Type Theory
Yasmine Shaorda
# Implementations of Dependent Type Theory

(Asked by: username_0 on 2019-12-04)

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.

**Tags:** type-theory, dependent-type
> **Comments:**
> **username_1**: 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.  
> **username_1**: 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.  
> **username_0**: @AndrejBauer Hello, I apologize if my question is off-topic. Do you have a recommendation of another venue for posting it?  
> **username_0**: 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.  
> **username_1**: 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](https://lists.seas.upenn.edu/mailman/listinfo/types-list).  
> **username_1**: And maybe some of the work of William Bowman could be relevant, see his [Gorwing a proof assistant](https://www.williamjbowman.com/resources/cur.pdf).  
> **username_2**: I think the most minimal you can get is Coq.  

---

## 0 answers

