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
21 votes
2 answers

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
9 votes
3 answers

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
24 votes
3 answers

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
11 votes
1 answer

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
6 votes
1 answer

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
6 votes
0 answers

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
5 votes
2 answers

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

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