Skip to main content

# Questions tagged [implementation]

Use this tag if you are implementing a proof engine, proof assistant or something similar in code. Do not use this tag if you are just at the design stage or asking about design decisions of existing code.

33 questions
Filter by
Sorted by
Tagged with
12 votes
1 answer
399 views

### Easy ways to introduce inductive types

I'm working up from elaboration zoo and noticed that you don't use fixed point if you've got type level computation. It causes unification/equality check to hang up. Now, this means that I need ...
4 votes
2 answers
199 views

### Binding variables to terms involving later variables

Consider the following pseudocode in a hypothetical proof assistant: def f (n : ℕ) : P n := match n with | zero -> ?0 | suc k -> ?1 end ...
-1 votes
1 answer
103 views

### Implementability of proof assistants for Infinitary logics with finite many terms

Infinitary logic is a natural consequence of extending the length of proofs of first-order logic to a infinite ordinal level. By definition, since proof lengths are infinitely long, one should not ...
19 votes
2 answers
1k views

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

I keep seeing these phrasing in some proof assistants/elaborators and their issues/internal discussions (e.g. Github search results in cooltt), that seems not that related to the actual proofs/...
2 votes
0 answers
121 views

### Implementation of cubical type theory as described in this paper?

Syntax and Models of Cartesian Cubical Type Theory I'd like to understand this paper enough to know how to implement cubical type theory. However I'm confused about how cofibrations should be ...
19 votes
1 answer
1k views

### When should I use De Bruijn levels instead of indices?

I am familiar with De Bruijn indices, but not with De Bruijn levels. In my understanding, indices index variables from the top of the context/stack, whereas levels index variables from the bottom. So ...
4 votes
1 answer
221 views

### Comparison of normal forms in Normalization by Evaluation

From what I understand of Normalization by Evaluation (NbE) as a technique to implement conversion, it 1) computes (some representation of) normal forms for each of the terms to compare, and 2) ...
2 votes
0 answers
101 views

### Is there a good demonstration of bidirectional type checking with strict Prop?

I've seen elaboration-zoo, pi-forall, Mini-TT, etc., all kinds of demonstrations of dependent type elaboration. However, none of them support Prop. I am interested ...
3 votes
1 answer
121 views

### Do implementations of a PA and of ATP have overlap?

I'm wondering how much overlap (read: code-reusage) there is between a PA and an ATP system. Are they based upon the same type system at least? I'm wondering, because right now I'm working on ...
0 votes
1 answer
124 views

### How do you implement what's in the Pierce Book precisely? And why / why not have evaluation just mutate ParseTree's of a PEG parser generator library?

Here is a link to the "Pierce Book" or Benjamin Pierce's draft transcript of (the first part of) "Types and Programming Languages". On PDF page 28 you'll see an OCaml ...
9 votes
3 answers
537 views

### How to implement a visual proof assistant?

Higher structures in category theory lead very organically to visual or graphical interpretations in terms of string diagrams and commuting squares. However, it seems hard to implement a graphical ...
5 votes
2 answers
226 views

### Algorithm for the locally nameless representation used by Lean

I have heard that Lean uses the locally nameless representation for handling binders, yet if I input an expression that has a bound variable in it, the bound variable is not displayed using its de ...
4 votes
3 answers
793 views

### 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? Here are some further details. I have a simple proof checker for ...
3 votes
1 answer
77 views

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

In cubical, hcomp is sometimes normal form, and to conversion check two normal hcomp terms, we need to compare the partial ...
2 votes
1 answer
78 views

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

Let h = hcomp (λ j → λ { (i = i1) → x }) u, using Cubical Agda syntax. The equivalent cubicaltt syntax is ...
7 votes
0 answers
159 views

### Tutorial implementations of extensional type theories

There are cool projects out there that covers the basic principles of implementing dependent type theories as very spartan proof assistants. These projects helped a lot when I learned about (...
11 votes
1 answer
276 views

### Normalization by evaluation for extensional type theories

Is there material on how to implement normalization for (any flavor of) ETT? This describes techniques related to doing untyped normalization. But there are (operational and semantic) problems when ...
7 votes
1 answer
318 views

### What is a neutral term?

A neutral/normal term in the lambda calculus is typically defined data nf = Lam of nf | Neu of ne data ne = Var of int | App of ne * nf Now the question is what to ...
2 votes
0 answers
109 views

### How to deal with axioms in a proof assistant?

I'm currently formalizing a little language which has somehow ended up looking a lot like Lawvere theories/finite product theories. I guess it's starting to look a little like Twelf? What I would love ...
10 votes
1 answer
291 views

7 votes
0 answers
146 views

### Could the Incredible Proof Machine work automatically with Metamath if rules of Metamath can be automatically translated into IPM custom logic blocks?

The Incredible Proof Machine (pdf) is a visual means of doing proofs. The Incredible Proof Machine can also be extended to do custom logics (Section 2.7 Custom logics). Metamath has thousands of ...
6 votes
1 answer
141 views

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

My question is based on this question, which asks about swapping out different SML implementations when building Isabelle. I've read on Wikipedia that Isaballe is written in Scala and SML. Based on ...
24 votes
3 answers
370 views

### What is the state of recompilation avoidance in proof assistants?

In compiler theory, there are multiple related, and often mixed, concepts that all help you compile code less often [1]: Already in the early times of FORTRAN (as of FORTRAN II [1, p. 384]), ...
4 votes
0 answers
132 views

### Are there any proof assistants that can not be derived from substitution?

Are there any type of proof systems that can not be implemented with substitution at the core? In essence if I want to implement a base library for building up various proof assistants do I only need ...