Questions tagged [reference-request]
Questions requesting papers or books in the literature on specific, narrow issues. Also consider the tag [recommendations].
25
questions
2
votes
0
answers
61
views
Have Hyperdoctrines been formalized?
I was thinking of formalizing them myself for a project if they haven't been already, and I looked in libraries and couldn't find anything.
I was thinking of coq in particular because it's the only ...
- 143
0
votes
0
answers
29
views
Simple and proper methods in Isar
https://isabelle.systems/cookbook/src/proofs/methods/Chained_Facts.thy
talks about
We note a slight difference. In the variant with intro, a trivial goal remains
that we need to solve by ‹assumption›....
- 267
2
votes
0
answers
66
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 ...
- 131
5
votes
1
answer
108
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
122
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, ...
- 517
1
vote
0
answers
168
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):
<...
- 517
9
votes
3
answers
472
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,768
2
votes
1
answer
192
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 ...
- 212
3
votes
2
answers
183
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.
- 419
7
votes
3
answers
372
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 ...
- 906
0
votes
0
answers
94
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,768
3
votes
0
answers
77
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
191
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,241
5
votes
3
answers
178
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,768
3
votes
1
answer
150
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,768
2
votes
1
answer
84
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,768
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 ...
- 7,240
6
votes
1
answer
238
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 ...
- 773
13
votes
3
answers
305
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,711
10
votes
1
answer
83
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,459
12
votes
3
answers
296
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
494
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 ...
- 7,240
27
votes
8
answers
728
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
123
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