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

6 votes
1 answer
162 views

How to implement a visual proof assistant?

13 votes
1 answer
381 views

When should I use De Bruijn levels instead of indices?

4 votes
2 answers
114 views

Algorithm for the locally nameless representation used by Lean

4 votes
3 answers
473 views

Creating a proof assistant for first order logic in Haskell

3 votes
1 answer
65 views

How does conversion check on partial elements/systems (in terms of cubical) work?

2 votes
1 answer
58 views

How does substitution on partial elements/systems (in terms of cubical) work?

7 votes
0 answers
109 views

Tutorial implementations of extensional type theories

10 votes
1 answer
168 views

Normalization by evaluation for extensional type theories

7 votes
1 answer
183 views

What is a neutral term?

2 votes
0 answers
81 views

How to deal with axioms in a proof assistant?

10 votes
1 answer
246 views

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

4 votes
1 answer
132 views

Tutorial implementation of analytic tableaux

13 votes
2 answers
450 views

Tutorial implementations of NbE

17 votes
2 answers
689 views

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

Browse more Questions