Skip to main content
Share Your Experience: Take the 2024 Developer Survey

Questions tagged [agda]

Agda is a dependently-typed programming language and a proof assistant.

Filter by
Sorted by
Tagged with
1 vote
1 answer
92 views

Formalising Church numerals in Agda

Beginer here. I'm trying to show that the closed $\beta$-nf's of type $ (\iota \to \iota) \to (\iota \to \iota) $ are the Church numerals ($\iota$ the base type, using the simply-typed lambda calculus)...
lfrg's user avatar
  • 13
4 votes
3 answers
149 views

Formalization of matching logic (logic behind K Framework)

Is there any mechanization for matching logic (any flavor)? I only find study about K Framework rules to Deducti translation, but this is both not covering to matching logic and not internalizing the ...
uhbif19's user avatar
  • 315
6 votes
1 answer
211 views

Is there a way to define dependent types without explicit substitutions internally within agda?

I am playing around the Programming Language Foundations in Agda exercises and wondering if we can achieve the same level of theories with dependent types. With simple types, the definition usually ...
Kaa1el's user avatar
  • 163
5 votes
1 answer
449 views

Example use cases for induction-recursion

I know of only two uses of induction-recursion: Encoding universes as a type, as shown in the Agda docs for recursion Encoding Finite sets as shown in Conor Mc'Bride's "datatypes of datatypes&...
Siddharth Bhat's user avatar
0 votes
2 answers
123 views

Pi-type over a list in dependent type theory

In a formalization I need to create an inductive type which has a term for each element in a list, something like this (I'll use Agda in the following, but everything here is standard dependent type ...
Max's user avatar
  • 113
18 votes
2 answers
2k views

Proof relevance vs. proof irrelevance

I want to use use Agda to help me write proofs, but I am getting contradictory feedback about the value of proof relevance. Jacques Carette wrote a Proof-relevant Category Theory in Agda library. But ...
Henry Story's user avatar
5 votes
0 answers
165 views

Non-trivial existence proof in type theory

What are some examples of existence proofs in Coq/Agda etc., where the constructed natural number is useful from mathematical point of view, but it's non-obvious from the proof what it should be? I am ...
Ilk's user avatar
  • 920
6 votes
0 answers
251 views

Postulating self types in a proof assistant

Self types introduce two typing new rules (simplified): $ \frac{\Gamma \; \vdash \; t : [t/x]T}{\Gamma \; \vdash \; t : \iota x. T}$ I-self and $ \frac{\Gamma \; \vdash \; t : \iota x. T}{\Gamma \; \...
Łukasz Lew's user avatar
  • 1,187
2 votes
1 answer
413 views

Extensional type theory and function extensionality

Is the principle of function extensionality $ (\forall x. f(x) = g(x)) \implies f = g$, derivable from ETT? Most notably is this derivable in Agda with axiom K?
Ilk's user avatar
  • 920
3 votes
0 answers
130 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 ...
Jacques Carette's user avatar
6 votes
1 answer
389 views

Small kernel (i.e. proof-verifier) for Agda?

Proof-assistants usually include a lot of machinery that assists in the creation of proofs. The creation process may be unsound without risking the soundness of the proof-assistant if the alleged ...
liwoxa's user avatar
  • 171
3 votes
1 answer
157 views

Formalization of dependent record types/kinds in MLTT or variant thereof?

Has anyone formalized Pollack's Dependently Typed Records in Type Theory ? Agda would be preferred, but anyone close to MLTT would work. Weaker versions would be fine too, i.e. what Luo dubs '...
Jacques Carette's user avatar
8 votes
0 answers
626 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 ...
Bob's user avatar
  • 381
5 votes
1 answer
339 views

Can a term on normal form prove an illogical assertion?

Suppose we take a language such as Agda and disable the features that make it consistent; for example, universe polymorphism, structural recursion checks and similar. Suppose then that we take a term ...
MaiaVictor's user avatar
  • 3,137
6 votes
1 answer
799 views

Is Church-pentation implementable in Agda?

Inspired by suggestion in this question, I've implemented predicative Church encoding of Peano arithmetic. Exponentiation works fine, unfortunately tetration requires the level of one of the arguments ...
Łukasz Lew's user avatar
  • 1,187
1 vote
0 answers
338 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: <...
Łukasz Lew's user avatar
  • 1,187
2 votes
1 answer
533 views

Is there a formalization of normalization of impredicative system F?

In particular Agda seems not strong enough to prove that. Is the predicative Calculus of Inductive Constructions universes (Coq without Prop) sufficient? How about with the impredicative Prop?
Łukasz Lew's user avatar
  • 1,187
9 votes
2 answers
328 views

How can you build a coinductive memoization table for recursive functions over binary trees?

The StreamMemo library for Coq illustrates how to memoize a function f : nat -> A over the natural numbers. In particular when ...
Russell O'Connor's user avatar
5 votes
3 answers
450 views

How to use Prop from UTT in Agda

In Ulf Norell's thesis he mentions that Agda is based on Luo's UTT. However, I can't find a way to use Prop there. Is there any way to do so?
Konstantin Solomatov's user avatar