All Questions
Tagged with termination dependent-type
2
questions
6
votes
2
answers
429
views
Possible root cause(s) of the misunderstanding that DTT implies not Turing complete?
I myself have fallen prey to this misconception, i.e., that being dependently typed as in Agda, Coq, etc., implies not being Turing complete, which can be (whether now or previously) found at quite a ...
10
votes
1
answer
249
views
Universe inconsistency as an effect
The Internet tells me there is some work on languages that permit general recursion but carry information about possible divergence in the type system. For instance, the simply-typed language Koka ...
- 3,200