gallais
  • Member for 9 years, 10 months
  • Last seen more than a month ago
"Minimal" intuitionistic type theory?
11 votes

The problem with Church encodings is that you cannot obtain induction principles for your types meaning that they are pretty much useless when it comes to proving statements about them. In terms of ...

View answer
Can a type system serve as a proof assistant for foreign functions?
Accepted answer
10 votes

Long story short: no you can't. A foreign function is like a black box and the type you ascribe to it is a promise you make: in the Curry-Howard correspondence that would correspond to adding an axiom ...

View answer
Proving a sorting operation in type system
7 votes

Twan van Laarhoven has a nice fully worked out example in Agda of the "Correctness and runtime of mergesort, insertion sort and selection sort". The comments are also interesting: in them, Bob Atkey'...

View answer
Agda: Which part does this type introduce universe inconsistency?
Accepted answer
6 votes

The term you're applying ¬_ to is large: it quantifies over all M : Set and therefore has type Set 1. So instead of ¬_ : Set -> Set you need ¬_ : Set 1 -> Set 1. A more general solution it to ...

View answer
Finite list induction principle and the tail eliminator
Accepted answer
3 votes

I am totally lost on how to approach this problem since the eliminator seems to be able to provide just function defined on the whole family List′A(n) and not on the sub-family List′A(s(n)). The ...

View answer
Meaning of $\mu t$ terms in dependent type theory
3 votes

The term μ t is the application of a closure μ to a term t. Similar to how t t' is the application of a term t to t'.

View answer
Clever memory management with constant time operations?
2 votes

You may want to have a look at amortized analysis and in particular dynamic arrays. Even if the operations are not really done in constant time at every step, in the long run it looks like it is the ...

View answer