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
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 ...
Julián's user avatar
  • 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›....
Gergely's user avatar
  • 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 ...
EGME's user avatar
  • 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 ...
Gabriele Cecilia's user avatar
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, ...
Ilk's user avatar
  • 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): <...
Ilk's user avatar
  • 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 ...
Molly Stewart-Gallus's user avatar
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 ...
Pietro Braione's user avatar
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.
user695931's user avatar
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 ...
Ana Borges's user avatar
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 ...
Molly Stewart-Gallus's user avatar
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?
Jacob woolcutt's user avatar
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 ...
Agnishom Chattopadhyay's user avatar
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 ...
Molly Stewart-Gallus's user avatar
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 ...
Molly Stewart-Gallus's user avatar
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 ...
Molly Stewart-Gallus's user avatar
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 ...
Jason Rute's user avatar
  • 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 ...
Joey Eremondi's user avatar
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 ...
Greg Nisbet's user avatar
  • 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 ...
Alex Nelson's user avatar
  • 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 ...
user9716869 - supports Ukraine's user avatar
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 ...
postmortes's user avatar
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 ...
Jason Rute's user avatar
  • 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 ...
ionchy's user avatar
  • 906