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.

7 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
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 (...
Trebor's user avatar
  • 3,947
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
0 answers
155 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
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
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 ...
Cheery's user avatar
  • 721
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 ...
ice1000's user avatar
  • 6,176
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 ...
Ms. Molly Stewart-Gallus's user avatar