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.
30
questions
4
votes
1
answer
155
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) ...
- 3,230
2
votes
0
answers
86
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 ...
- 5,424
3
votes
1
answer
93
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
95
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 ...
7
votes
3
answers
389
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 ...
- 2,628
4
votes
2
answers
146
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 ...
- 399
4
votes
3
answers
553
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 ...
- 399
3
votes
1
answer
69
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 ...
- 5,424
2
votes
1
answer
65
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 ...
- 5,424
7
votes
1
answer
202
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,051
11
votes
1
answer
198
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 ...
- 3,261
2
votes
0
answers
93
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 ...
- 2,628
4
votes
1
answer
134
views
Tutorial implementation of analytic tableaux
I am re-reading John Harrison's wonderful Handbook of Practical Logic and Automated Reasoning, and he has a rather idiosyncratic presentation of analytic tableaux.
What other tutorial implementations ...
- 1,439
7
votes
0
answers
126
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 (...
- 3,261
10
votes
1
answer
259
views
How to implement the type checking of `transp` in de Morgan cubical type theory?
I am reading many referential materials and I want to find a proper way to implement it. Suppose the syntax is ${\sf transp}~A~\psi:A~0\to A~1$, where (let's call it "the condition") $A:\...
- 5,424
17
votes
2
answers
763
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/...
- 181
13
votes
2
answers
489
views
Tutorial implementations of NbE
For a project I'm planning on doing with some students this summer, I'm looking for an implementation of normalization-by-evaluation whose code the students can read, understand, and extend. So I'd ...
- 2,832
10
votes
1
answer
236
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 ...
- 671
6
votes
0
answers
146
views
Is there a consolidated or partial list noting the use of quasiquotation with provers?
In checking to see if any provers (proof assistants, theorem provers, interactive theorem prover) make use of quasiquotation I was quickly surprised at what started showing up with a Google search.
...
- 2,796
14
votes
1
answer
708
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 ...
- 2,051
4
votes
2
answers
167
views
Can a proof engine be built based on graphs?
One of the more common ways to do proofs is using a deductive system.
Can proofs instead be done using graphs?
I am seeking papers that outline from the ground up how such a system works. If example ...
- 2,796
5
votes
1
answer
100
views
How to elaborate with dependent records present?
Dependent records can be implemented in various ways, but some papers suggests I could do it in the following way:
The construction of dependent record type is made by selecting labels and types.
The ...
- 671
3
votes
0
answers
66
views
Variable binding techniques used in proof assistants? [duplicate]
There are many resources (1, 2, 3, 4) to learn about various techniques for manipulating syntax with variable binding, however, I haven't seen many descriptions of which specific techniques are ...
7
votes
0
answers
133
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 ...
- 2,796
5
votes
1
answer
102
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 ...
- 2,651
7
votes
1
answer
135
views
Implementation details of implicit arguments
How do the implicit arguments work in proof assistants such as Agda or Coq? Specifically, how are the blanks filled in? What kind of resolution algorithm is used?
Are there any papers written about ...
- 671
19
votes
2
answers
388
views
What difficulties are there in basing a proof assistant on the $\lambda\mu$-calculus and has any proof assistant tried?
The $\lambda\mu$-calculus is a variant of the $\lambda$ calculus introduced by Parigot to capture classical logic. The Wikipedia article describing it in more detail is here. In modern proof ...
- 809
24
votes
3
answers
311
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]), ...
- 1,602
4
votes
0
answers
126
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 ...
- 2,796
9
votes
2
answers
315
views
What makes a proof assistant a proof assistant?
In doing research for my next question was going to reference another post in CS Stack Exchange. After reading the answers decided they did not go into enough detail, they leave one with more ...
- 2,796