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, 7 months
  • Last seen more than a week ago
Profile Activity

21 Answers

Score Activity Newest
2 votes

Stream of all finite prefixes of a stream

2 votes

Stacks versus universes

8 votes
Accepted

What are the advantages to impredicativity?

4 votes
Accepted

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

21 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?

5 votes

Is there computational interpretation for countable choice?

14 votes
Accepted

What axioms have a computational interpretation?

5 votes
Accepted

Is unguarded fixpoint reduction consistent?

15 votes
Accepted

Incorporating Markov's principle in various proof assistants

17 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?

13 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?

17 votes
Accepted

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

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.