Questions tagged [reference-request]
Questions requesting papers or books in the literature on specific, narrow issues. Also consider the tag [recommendations].
23
questions
2
votes
0
answers
49
views
Formalization of Analytic Number Theory
Is there any formalization, in any proof checking environment (Lean, Isabelle, etc.) of basic analytic number theory, say everything in a book like the Titchmarsh book (The Theory of the Riemann Zeta ...
- 121
4
votes
0
answers
54
views
Is there any formalization (with any theorem prover) of the Bohm theorem for lambda-calculus?
I am an university student working on a thesis about λ-calculus. I'd like to know if there's any article or publication about proof assistant formalizations of the Bohm theorem ("any two normal ...
3
votes
0
answers
117
views
Uniform notions of pattern matching at dependent types with impredicative proof strength
I am looking for axioms/inference rules that satisfy the following 3 conditions:
can be added to predicative intensional Martin-Löf type theory, so $\Pi$, $\Sigma$, equality type, with W-types, ...
- 497
1
vote
0
answers
159
views
Descriptions of heterogenous datatypes
When attempting to describe the datatype as appearing in my previous question, using indexed descriptions in style of The Gentle Art of Levitation to describe this datatype (using Agda for examples):
<...
- 497
7
votes
3
answers
389
views
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 ...
- 2,628
2
votes
1
answer
156
views
What are references for learning type theory?
What could be a good set of references for starting to learn type theory? We can assume that the students have a computer science background but not specifically on functional programming or lambda ...
- 186
2
votes
2
answers
166
views
Reference request for an introduction to higher-order logic
I'm looking for an introductory text or other materials on higher order logic, with a minimum of assumed background knowledge beyond first order logic.
- 399
8
votes
3
answers
305
views
Has anyone accidentally "proven" a false theorem using what was later found to be a critical bug?
Critical bugs are periodically found in Coq, and I assume in other proof assistants as well. We are still happy to mostly trust the proof assistants, partly because these critical bugs are relatively ...
- 874
0
votes
0
answers
86
views
Existential variables in dependent type theory
For the kernel of a proof assistant free variables/universal quantification may be sufficient. In higher level languages such as Coq's tactic language indeterminate variables (not sure of the wording ...
- 2,628
3
votes
0
answers
68
views
Where is the discriminate tactic defined in Coq?
One can read the Coq documentation about discriminate tactic here.
Were is this tactic actually defined?
6
votes
1
answer
149
views
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 ...
- 1,095
3
votes
3
answers
135
views
Mechanization of game semantics?
Is there any work on mechanization of game semantics?
I have no experience in this area but game semantics are supposed to provide interesting denotational semantics for a variety of programming ...
- 2,628
3
votes
1
answer
139
views
Is there any work on the use of free logic in proof assistants?
I've been reading up on free logic. I have a hunch it could be useful for type theory. For example, the fixed point of an expression might not always exist or an expression might not be well typed in ...
- 2,628
2
votes
1
answer
75
views
Use of modal logic in metaprogramming
I know modal logic has been experimented with for formalizing macros and metaprogramming before but I am not really familiar with the details. I would like to read up more on the use of modal logic ...
- 2,628
6
votes
3
answers
3k
views
What are good examples of April fools jokes in the proving assistant community?
Every community can have inside jokes among it, and April Fool’s jokes are a common variety, but proof assistants are particularly susceptible to April Fool’s jokes. They have strong guarantees of ...
- 5,748
6
votes
1
answer
221
views
Parameterized Datatypes in a Universe à la Tarski?
I'm wondering, is there a way to make a Universe à la Tarski that models all of the types in an open type theory, where there can be user defined parameterized inductive types?
For context, I'm trying ...
- 653
13
votes
3
answers
267
views
What are the possible kinds of type theories or logics with quotients?
As described in this answer, one of the differences between Coq and Lean is the presence of definitional quotients in the latter. By contrast, the absence of definitional quotients in Coq forces one ...
- 2,651
10
votes
1
answer
78
views
Reasoning with the definition of Standard ML
I know that the definition of Standard ML has been mechanized in Twelf, but are there tools which allow me to verify my Standard ML code satisfies certain properties or specifications?
I'm vaguely ...
- 1,439
12
votes
3
answers
279
views
PDEs and proof assistants
I would like to know if there are any ongoing or completed projects in the area of the verification of the numerical methods for PDEs or the exposition of (any aspects of) the traditional PDE theory ...
20
votes
9
answers
453
views
What are good books for learning about proof assistants for Functional Analysis?
I did search on the site already and while there are questions that reference, for example, PLFA for Agda, there doesn't seem to be a canonical list of references for people just learning about proof ...
- 319
17
votes
0
answers
149
views
What are the major formal mathematics libraries and how big are they? [duplicate]
Every major theorem prover has one or more libraries of general mathematics. I'm curious where these libraries are and what their current statistics are (for example, how many theorems do they ...
- 5,748
27
votes
8
answers
568
views
Where can I find lists of theorems that have been verified?
I recall many years ago seeing a very large and well-interlinked (by computer) list of verified results starting from base assumptions and leading to all sorts of things that naive me did not expect ...
14
votes
2
answers
118
views
Formal description of algorithmic subtyping/cumulativity
Are there any references (papers, documentation, etc.) for how proof assistants with subtyping due to cumulativity actually implement algorithmic subtyping? Coq, for instance, has subtyping, but the ...
- 906