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.

Filter by
Sorted by
Tagged with
0 votes
1 answer
8 views

How to implement separate compilation?

This feels like a really basic question, but I haven't been able to find an answer to it. How should a proof assistant implement separate compilation? Maybe the answer is "just like any ...
Mike Shulman's user avatar
  • 3,170
2 votes
0 answers
78 views

Lower bounds in type theory proof assistant with ordinals and universes without axioms

I saw a PowerPoint that claimed to achieve $\psi_0(\Gamma_{\Omega+1})$ in Agda without any axioms. I was wondering if a better lower bound exists in 2024? My ...
Ember Edison's user avatar
4 votes
2 answers
205 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 ...
Mike Shulman's user avatar
  • 3,170
-1 votes
1 answer
104 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 ...
Ember Edison's user avatar
2 votes
0 answers
123 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 ...
Cheery's user avatar
  • 721
4 votes
1 answer
233 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) ...
Meven Lennon-Bertrand's user avatar
2 votes
0 answers
103 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 ...
ice1000's user avatar
  • 6,256
3 votes
1 answer
122 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 ...
HighAsAKiteOnMath's user avatar
0 votes
1 answer
128 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 ...
HighAsAKiteOnMath's user avatar
9 votes
3 answers
549 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 ...
Ms. Molly Stewart-Gallus's user avatar
5 votes
2 answers
229 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 ...
user695931's user avatar
4 votes
3 answers
801 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 ...
user695931's user avatar
3 votes
1 answer
79 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 ...
ice1000's user avatar
  • 6,256
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 ...
ice1000's user avatar
  • 6,256
7 votes
1 answer
322 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 ...
Couchy's user avatar
  • 2,241
11 votes
1 answer
282 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 ...
Trebor's user avatar
  • 4,005
2 votes
0 answers
111 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 ...
Ms. Molly Stewart-Gallus's user avatar
4 votes
1 answer
150 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 ...
Alex Nelson's user avatar
  • 1,564
7 votes
0 answers
162 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 (...
Trebor's user avatar
  • 4,005
10 votes
1 answer
293 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:\...
ice1000's user avatar
  • 6,256
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/...
Anqur's user avatar
  • 301
14 votes
2 answers
554 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 ...
Mike Shulman's user avatar
  • 3,170
12 votes
1 answer
401 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 ...
Cheery's user avatar
  • 721
6 votes
0 answers
156 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. ...
Guy Coder's user avatar
  • 2,846
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 ...
Couchy's user avatar
  • 2,241
4 votes
2 answers
192 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 ...
Guy Coder's user avatar
  • 2,846
5 votes
1 answer
128 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 ...
Cheery's user avatar
  • 721
3 votes
0 answers
68 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 ...
Alexander Gryzlov's user avatar
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 ...
Guy Coder's user avatar
  • 2,846
6 votes
1 answer
147 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 ...
Greg Nisbet's user avatar
  • 2,819
8 votes
1 answer
177 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 ...
Cheery's user avatar
  • 721
21 votes
2 answers
546 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 ...
Andrew Marmaduke's user avatar
24 votes
3 answers
371 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]), ...
Sebastian Ullrich's user avatar
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 ...
Guy Coder's user avatar
  • 2,846
9 votes
2 answers
420 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 ...
Guy Coder's user avatar
  • 2,846