Skip to main content
Pierre-Marie Pédrot's user avatar
Pierre-Marie Pédrot's user avatar
Pierre-Marie Pédrot's user avatar
Pierre-Marie Pédrot
  • Member for 2 years, 3 months
  • Last seen this week
2 votes

Stream of all finite prefixes of a stream

2 votes

Stacks versus universes

4 votes
Accepted

Does quantification over functions (STLC) increase strength beyond first order logic?

24 votes
Accepted

Why not have `Prop : Set` in Coq?

3 votes

Turning off some sProp checks

11 votes
Accepted

What axioms do I need to search the naturals?

5 votes
Accepted

Does Coq's Module and Functor type-check incrementally?

13 votes

Is there any example of a dependent product that makes sense in a non-type-theory context?

8 votes
Accepted

What are the advantages to impredicativity?

5 votes

Is there computational interpretation for countable choice?

15 votes
Accepted

What axioms have a computational interpretation?

5 votes
Accepted

Is unguarded fixpoint reduction consistent?

16 votes
Accepted

Incorporating Markov's principle in various proof assistants

19 votes

What exactly is setoid hell?

9 votes

Can a proof engine be built based on graphs?

8 votes

What's the relationship between refinement types and dependent types?

10 votes

What's the difference between a universe level and a natural number?

15 votes

What difficulties are there in basing a proof assistant on the $\lambda\mu$-calculus and has any proof assistant tried?

8 votes

Can the development of proof assistants make mathematicians switch their framework?

7 votes
Accepted

Are there any provers based on a paraconsistent logic?

18 votes
Accepted

What is the state of coinductive types and reasoning in Coq?