Proof Assistants Beta
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 1 year, 10 months
  • Last seen more than a week ago
Profile Activity

21 Answers

Score Activity Newest
21 votes
Accepted

Why not have `Prop : Set` in Coq?

18 votes
Accepted

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

18 votes

What exactly is setoid hell?

15 votes
Accepted

Incorporating Markov's principle in various proof assistants

14 votes
Accepted

What axioms have a computational interpretation?

13 votes

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

13 votes

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

11 votes
Accepted

What axioms do I need to search the naturals?

10 votes

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

9 votes

Can a proof engine be built based on graphs?

8 votes

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

8 votes

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

8 votes
Accepted

What are the advantages to impredicativity?

7 votes
Accepted

Are there any provers based on a paraconsistent logic?

5 votes
Accepted

Is unguarded fixpoint reduction consistent?

5 votes
Accepted

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

5 votes

Is there computational interpretation for countable choice?

4 votes
Accepted

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

3 votes

Turning off some sProp checks

2 votes

Stacks versus universes

2 votes

Stream of all finite prefixes of a stream

Your privacy

By clicking “Accept all cookies”, you agree Stack Exchange can store cookies on your device and disclose information in accordance with our Cookie Policy.