Skip to main content
22 votes
Accepted

When should I use De Bruijn levels instead of indices?

If we want to do evaluation in the presence of free variables ("open" evaluation), then De Bruijn levels are essential, precisely because of their support for cost-free weakening. Generally, ...
András Kovács's user avatar
17 votes
Accepted

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

TL; DR: There are. But there are also severe difficulties that only have unsatisfactory solutions. Let's see what bad things will happen, so we can attempt to fix it. The first thing when trying to ...
Trebor's user avatar
  • 3,867
16 votes
Accepted

Easy ways to introduce inductive types

In principle, every indexed inductive type can be defined from $\bot$, $\top$, $\mathsf{Bool}$, $\Pi$, $\Sigma$, $\mathsf{W}$, $\mathsf{Id}$ and universes, with exactly the expected eliminators and ...
András Kovács's user avatar
14 votes

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

I think that the first question can be generalized to "What difficulties are there in adding side-effects to a proof assistant based on dependent type theory." First-class continuations are ...
Pierre-Marie Pédrot's user avatar
13 votes
Accepted

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

So, first, the origin of this term in the context of cubical type theory comes from its intended semantics, which are in turn inspired by the model-categorical semantics of homotopy type theory. Let's ...
daniel gratzer's user avatar
13 votes

Tutorial implementations of NbE

Daniel Gratzer has written two tutorial implementations of normalization by evaluation in OCaml: https://github.com/jozefg/nbe-for-mltt: plain MLTT with universes https://github.com/jozefg/blott: a ...
Jonathan Sterling's user avatar
9 votes
Accepted

How to implement a visual proof assistant?

Your question is pretty broad. How would I implement and reason about a graphical calculus or proof assistant? First (almost tautologically) I think you need to carefully consider two questions: ...
Jason Rute's user avatar
  • 8,555
9 votes
Accepted

What is a neutral term?

A neutral term is a variable, or an eliminator stuck on a neutral term. Basically a stack of eliminators applied to a variable. These terms are called neutral, and distinguished from other normal ...
Matthew McQuaid's user avatar
9 votes

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

Let me provide a slightly watered up supplement of Gratzer's answer. In the beginning, mathematicians need to study spaces by considering how other spaces cover(*) them. For example, if you have a ...
Trebor's user avatar
  • 3,867
9 votes

Can a proof engine be built based on graphs?

Your question is quite vague, but can be answered positively when taken literally. Indeed, most implementations of a deductive system are actually already using graphs internally. When phrased ...
Pierre-Marie Pédrot's user avatar
7 votes

What is the state of recompilation avoidance in proof assistants?

Lean (in any version) at the time of writing does not really implement any sort of recompilation avoidance beyond the make approach. In particular, the produced <...
Sebastian Ullrich's user avatar
7 votes
Accepted

Normalization by evaluation for extensional type theories

For many partial languages, although conversion is undecidable, we can decide conversion up to non-termination. For example, in pure LC, conversion is decidable for the $\beta$-normalizing terms. In ...
András Kovács's user avatar
7 votes

Binding variables to terms involving later variables

Great question Mike! Since Thierry Coquand's talk at the 1991 TYPES meeting in Edinburgh, and reading Martin Löf's "Mathematics of infinity" paper, and various things by Thierry subsequently,...
James McKinna's user avatar
6 votes

Algorithm for the locally nameless representation used by Lean

I implemented the spartan type theory as an educational tool for people who are interested in implementing their own formal systems. If you look at how the type of expressions ...
Andrej Bauer's user avatar
  • 8,989
6 votes
Accepted

Do implementations of a PA and of ATP have overlap?

Unfortunately there is much less code reuse possible than one would hope. There three levels to consider: Differences between mathematical foundations (and implementations) between proof assistants. ...
Anja Petković Komel's user avatar
5 votes

How to implement a visual proof assistant?

A graphical proof assistant for higher categories under active development is homotopy.io, which follows the tradition of Globular. The underlying notion of higher structure used by homotopy.io is ...
Maximilian Doré's user avatar
5 votes
Accepted

Tutorial implementation of analytic tableaux

As far as I'm aware, leanTAP was written in just a few lines of Prolog, and it works with first-order formulas in Skolem normal forms. There's a tutorial implementation in OCaml which looks similar to ...
Zhanrong Qiao's user avatar
5 votes
Accepted

Can a proof engine be built based on graphs?

Well, a proof engine is built atop a proof calculus, right? And natural deduction basically amounts to using a specific set of possible labeled edges in graphs for proofs (namely, introduction and ...
Alex Nelson's user avatar
  • 1,564
5 votes

What is the state of recompilation avoidance in proof assistants?

For metamath, we store a detailed set of proof steps for each theorem or lemma along with what we are proving. As you describe in your discussion of systems which don't export their proofs, it is the ...
Jim Kingdon's user avatar
5 votes

What is the state of recompilation avoidance in proof assistants?

Agda has a very rudimentary form of caching of the current file, where it does not have to recheck the initial part of a file that has not changed since the last reload. See https://github.com/agda/...
Jesper's user avatar
  • 486
5 votes
Accepted

Comparison of normal forms in Normalization by Evaluation

I will present the conversion procedure that is used in András Kovács' Elaboration zoo and its extension to the η-rule for the unit type. It is based on Coquand's type-checking algorithm. In ...
Rafaël Bocquet's user avatar
5 votes

Binding variables to terms involving later variables

Coq (and probably Lean too): The answer for (vanilla) Coq is simple: it does not. Nothing is done to n to remember its relation to the pattern in the branch. The ...
Meven Lennon-Bertrand's user avatar
4 votes

What makes a proof assistant a proof assistant?

Since this question made it back up to the top, let me take a stab. In short, there is going to be no air-tight definition of a "proof assistant" just like there is no air-tight definition ...
Jason Rute's user avatar
  • 8,555
4 votes
Accepted

Architecture of Isabelle: What parts are written in SML? What parts are written in Scala? What does the boundary look like?

Scala appears to use the JVM, and this has been marketed as a feature, not a bug. According to Isabelle/Scala: Isabelle/ML is for ‹mathematics›, to develop tools within the context of symbolic logic, ...
Alex Nelson's user avatar
  • 1,564
4 votes
Accepted

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

For example, if $i∧j∨k∧(¬l)=1$, then what? What should I do to $A$? As Trebor said, for $ i_1 ∧ i_2 ∧ … ∧ i_n = 1 $ we should perform n substitutions and check that $ A(i_1/1, i_2/1, …, i_n/1) = A(...
siegment's user avatar
  • 272
4 votes
Accepted

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

In other words, does substitution on partial elements create more clauses? Do they share the same clause body? Yes, you may check both in Cubical Agda: ...
siegment's user avatar
  • 272
3 votes

Creating a proof assistant for first order logic in Haskell

I am planning to implement a FOL proof assistant in Haskell. What are some useful libraries and implementations I should be looking at? Does this do the Haskell part of what you need? I ask because ...
Guy Coder's user avatar
  • 2,836
3 votes

Creating a proof assistant for first order logic in Haskell

Here's what uncle Google gave me: Refinement Reflection (or, how to turn your favorite language into a proof assistant using SMT). hout: Non-interactive proof assistant monad for first-order logic. ...
Andrej Bauer's user avatar
  • 8,989
3 votes
Accepted

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

In the paper about Cubical Agda you may find that partial elements Partial r A “are equal whenever they reduce to equal terms for all the possible assignment of ...
siegment's user avatar
  • 272
3 votes

Tutorial implementations of NbE

Does code in paper format count? In which case I would throw in Danvy, Keller, and Puech's Typeful Normalization by Evaluation You get an intro to deep vs. shallow, an analogy with printf, and an ...
gallais's user avatar
  • 1,126

Only top scored, non community-wiki answers of a minimum length are eligible