Questions tagged [agda]

The tag has no usage guidance.

3 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
6
votes
0answers
158 views

An axiom for John Major's Equality

In the the standard library of Coq, there is the axiom: Axiom JMeq_eq : forall (A:Type) (x y:A), JMeq x y -> x = y. Why isn't it provable? Can it be reduced ...
2
votes
0answers
87 views

Have the proofs in Buss's “On Goedel’s Theorems on Lengths of Proofs” been formalized (mechanically checked)?

The paper On Gödel's theorems on lengths of proofs I: Number of lines and speedup for arithmetics contains quite interesting results on proof length. But some of the details are still, to me, a bit ...
1
vote
0answers
225 views

Is it possible to type Ackermann function with (stratified variant of) System F?

I was surprised to find no open-source implementation of Ackermann function in pure System F as an illustrative example. I finally managed to implement it myself in Haskell using Church encoding: <...