Questions tagged [reference-request]

Questions requesting papers or books in the literature on specific, narrow issues. Also consider the tag [recommendations].

Filter by
Sorted by
Tagged with
2 votes
0 answers

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

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

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

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

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 votes
1 answer

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 ...
2 votes
2 answers

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.
8 votes
3 answers

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 ...
0 votes
0 answers

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 ...
3 votes
0 answers

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

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 ...
3 votes
3 answers

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 ...
3 votes
1 answer

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 votes
1 answer

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 ...
6 votes
3 answers

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

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 ...
13 votes
3 answers

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

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

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

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 ...
17 votes
0 answers

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

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

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