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
6 votes
1 answer
150 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 ...
user avatar
  • 1,662
9 votes
1 answer
141 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 ...
user avatar
  • 2,246
3 votes
0 answers
73 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 ...
user avatar
4 votes
1 answer
128 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 ...
user avatar
  • 1,357
7 votes
0 answers
95 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 (...
user avatar
  • 2,246
10 votes
1 answer
223 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:\...
user avatar
  • 4,136
13 votes
2 answers
606 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/...
user avatar
  • 141
14 votes
2 answers
434 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 ...
user avatar
  • 2,079
10 votes
1 answer
165 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 ...
user avatar
  • 651
6 votes
0 answers
139 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. ...
user avatar
  • 2,676
12 votes
1 answer
222 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 ...
user avatar
  • 1,662
4 votes
2 answers
153 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 ...
user avatar
  • 2,676
4 votes
1 answer
89 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 ...
user avatar
  • 651
2 votes
0 answers
59 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 ...
user avatar
6 votes
0 answers
111 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 ...
user avatar
  • 2,676
4 votes
1 answer
73 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 ...
user avatar
  • 2,467
6 votes
1 answer
118 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 ...
user avatar
  • 651
18 votes
2 answers
282 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 ...
user avatar
22 votes
3 answers
253 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]), ...
user avatar
4 votes
0 answers
116 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 ...
user avatar
  • 2,676
9 votes
2 answers
289 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 ...
user avatar
  • 2,676