Questions tagged [recommendations]

Use this for questions seeking an asset that give nebulous criteria rather than concrete specifics. If seeking literature such as books or papers use [tag:reference-request]. If seeking software use [tag:software-request].

Filter by
Sorted by
Tagged with
4 votes
3 answers

Why use records for non-empty lists rather than inductively defined non-empty lists?

I've come across two main ways to do non-empty lists: ...
  • 141
6 votes
1 answer

What are some good resources for Proof Assistant based exercises/puzzles for recreation and practice?

Proof Assistant based exercises and puzzles make for a good recreational activity, as well as help sharpen skills of users of said systems. There are many such equivalent resources for algorithmic ...
8 votes
1 answer

How to deal with the proliferation of encodings of ASTs?

When working with type theory and ASTs one often ends up with a large amount of different encodings. It's very similar to the same problem in compiler design but more annoying because it's dependently ...
16 votes
1 answer

Formalizations of unsolved problems

Is there a library (for any proof assistant) which provides formalized definitions of unsolved problems? To clarify, I mean some collection that correctly defines unsolved problems in the language of ...
  • 519
13 votes
2 answers

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 ...
  • 2,802
7 votes
1 answer

Type Theory research groups

Research about type theory, internal languages, intuitionism, constructivism, and proof assistants is, at the moment, not as fashionable as other branches of mathematics are, say for example algebraic ...
  • 640
13 votes
2 answers

verifying combinatorial constructions - choice of a proof assistant

The choice of the proof assistant to use for formalisation depends on the area quite a bit; e.g. they say that algebraic topology comes easy in HoTT assistants. What would be the most natural choices ...
14 votes
4 answers

What mathematical topics should I learn first before I start using proof assistants?

I'm a theoretical computer scientist and my research is focused mainly on structural and algorithmic graph theory. Recently I've been very interested in using proof assistants. As a "pet project&...
5 votes
1 answer

General Guidelines and Tips for using Induction

There are many kinds of induction (induction over the natural numbers ⊂ structural induction ⊂ Noetherian induction), when do I use which flavour? And what should I keep in mind when doing proofs by ...
  • 1,088
3 votes
1 answer

How could I make a Proof Assistant? [closed]

If, as a complete beginner, I wanted to create a proof assistant, how would I begin to start this? How easy is one to create? What advice do you have? Note: contains "multiple questions" as ...
  • 1,258
17 votes
2 answers

How to deal with Binders?

When reasoning about programming languages in a deep embedding, $\alpha$-equivalence, binders and capture-avoiding substitution quickly can become tedious. Complex binders may introduce multiple bound ...
  • 1,088
10 votes
1 answer

Is there an official recommendation for editors to input Lean unicode characters?

As mentioned in another question, the way that VSCode and other editors implement unicode characters that cannot be typed directly from most keyboards is an editor feature. As such, different editors ...