13
votes
Tutorial implementations of NbE
Daniel Gratzer has written two tutorial implementations of normalization by evaluation in OCaml:
https://github.com/jozefg/nbe-for-mltt: plain MLTT with universes
https://github.com/jozefg/blott: a ...
10
votes
Formalizations of unsolved problems
The closest to what you are asking for might be the Formal abstracts project whose aim is to formalize the statements (but no proofs) of results from papers.
Formalizing statements without proofs is ...
- 11k
9
votes
Accepted
Is there an official recommendation for editors to input Lean unicode characters?
Because maintaining such a big list of Unicode abbreviations is annoying and none of the editor mode maintainers are interested in encouraging untransferrable abbreviations, as far as I know, all of ...
- 1,809
8
votes
Accepted
Learning category theory from Lean formalization?
I recommend learning category theory from humans, and if those are not avaiable then from books. It is a feature of category theory that it draws examples from a wide range of mathematics, which is ...
- 11k
7
votes
Accepted
verifying combinatorial constructions - choice of a proof assistant
If I understand you correctly, you will be working with finite discrete objects, such as finite fields, finite groups, finite combinatorial objects, etc. I would recommend using a proof assistant ...
- 11k
7
votes
Accepted
What mathematical topics should I learn first before I start using proof assistants?
I came to proof assistants from TCS about a year ago, so perhaps I am well placed to answer your question. This may be somewhat opinion-based, but I don't feel it is necessary to learn category theory ...
- 716
7
votes
Accepted
How to deal with Binders?
There are already a lot of choices pointed out on Jesper Cockx's blog. Usually, the properties you would like to establish includes
Equations of compositions of substitutions. For example, $E[x/A][y/...
- 4,344
6
votes
Accepted
How could I make a Proof Assistant?
There are many good resources, such as the little prover book, "A tutorial implementation
of a dependently typed lambda calculus" tutorial, "A simple type-theoretic language: Mini-TT&...
- 6,532
6
votes
What mathematical topics should I learn first before I start using proof assistants?
I would say the most confusing (and often frustrating) notion for many first users is that types are not sets, so unless you plan on using a proof assistant specifically based on set theory (almost ...
- 2,330
6
votes
Accepted
How to deal with the proliferation of encodings of ASTs?
As various commenters have said, you sometimes just need to bite the bullet. Good modularity, good naming conventions and other standard good software practices will help. If you need inspiration, I'...
- 1,142
4
votes
Type Theory research groups
External links
The following pages mention researchers interested in the foundations or applications of proof assistants:
Authors participating in the TYPES international conference on Types for ...
4
votes
verifying combinatorial constructions - choice of a proof assistant
I moved this answer to Proof assistants for beginners - a comparison, since it is general advice. However, I still do think it applies to your circumstance. In particular, it is not clear in your ...
- 10.3k
4
votes
What mathematical topics should I learn first before I start using proof assistants?
Here are some topics I would recommend learning:
Some Functional Programming. I think it is good to learn some functional programming language. Preferably some language which takes immutability ...
- 1,502
3
votes
Why use records for non-empty lists rather than inductively defined non-empty lists?
Since nelist_b is based on pre-existing lists, you can presumably reuse a lot of results on lists when proving facts about ...
- 946
3
votes
General Guidelines and Tips for using Induction
The best guideline is: If you don't know how to do the proof on pen-and-paper, you probably will get lost doing it in a proof assistant. If you don't know what your induction hypothesis is supposed ...
- 1,607
3
votes
What mathematical topics should I learn first before I start using proof assistants?
Unlike the other answers, I'm fairly convinced you do not need to learn anything (category theory, type theory, functional programming, or even logic) before hand. I have two basic reasons for this. ...
- 10.3k
3
votes
Tutorial implementations of NbE
Does code in paper format count? In which case I would throw in
Danvy, Keller, and Puech's Typeful Normalization by Evaluation
You get an intro to deep vs. shallow, an analogy with printf, and an ...
- 1,264
2
votes
What are some good resources for Proof Assistant based exercises/puzzles for recreation and practice?
You already mention two very complete sites of exercises and I don’t have much reason to think there are more of that kind. In particular, Proving For Fun hosts the proving competition Proof Ground ...
- 10.3k
1
vote
Why use records for non-empty lists rather than inductively defined non-empty lists?
You could also try to use dependently typed sequences (I'm using the Mathematical Components library here), as in:
...
- 281
1
vote
How to deal with Binders?
This is kind of silly but I haven't really seen it concretely written down anywhere.
Given a system of first-order logic you don't need to have a concrete system of terms at all but can only use ...
- 2,898
Only top scored, non community-wiki answers of a minimum length are eligible