All Questions
Tagged with agda dependent-type
3
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 ...
6
votes
1
answer
409
views
What are the principal differences between Agda's core type theory and Coq's?
Agda is said to be based on Luo's unifying theory of dependent types while Coq is based on the Calculus of Inductive Constructions. Both of these as I understand it extend the impredicative ...
16
votes
2
answers
404
views
What are the upsides and downsides of typed vs untyped conversion?
What are the tradeoffs between untyped and type-directed conversion in dependent type theory, and is there any consensus on what's "better"?
Background
Generally speaking, in dependent type ...
- 394