Proof Assistants Stack Exchange is a question and answer site for mathematicians and computer scientists who develop and use proof assistants. It only takes a minute to sign up.

Sign up to join this community
Anybody can ask a question
Anybody can answer
The best answers are voted up and rise to the top

Explore our Questions

7 votes
0 answers
95 views

Tutorial implementations of extensional type theories

9 votes
1 answer
141 views

Normalization by evaluation for extensional type theories

6 votes
1 answer
150 views

What is a neutral term?

3 votes
0 answers
73 views

How to deal with axioms in a proof assistant?

10 votes
1 answer
223 views

How to implement the type checking of `transp` in de Morgan cubical type theory?

4 votes
1 answer
128 views

Tutorial implementation of analytic tableaux

14 votes
2 answers
434 views

Tutorial implementations of NbE

13 votes
2 answers
606 views

What are "fibration/cofibration" in type theory and what are their intuitions?

6 votes
0 answers
139 views

Is there a consolidated or partial list noting the use of quasiquotation with provers?

9 votes
2 answers
289 views

What makes a proof assistant a proof assistant?

10 votes
1 answer
165 views

Easy ways to introduce inductive types

12 votes
1 answer
222 views

When should I use De Bruijn levels instead of indices?

4 votes
2 answers
153 views

Can a proof engine be built based on graphs?

4 votes
1 answer
89 views

How to elaborate with dependent records present?

Browse more Questions