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
4 votes
1 answer
78 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 ...
user avatar
3 votes
3 answers
100 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 ...
user avatar
2 votes
1 answer
79 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 ...
user avatar
4 votes
1 answer
63 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 ...
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 ...
user avatar
  • 3,720
6 votes
1 answer
176 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 ...
user avatar
13 votes
3 answers
237 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 ...
user avatar
  • 2,509
10 votes
1 answer
71 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 ...
user avatar
  • 1,409
12 votes
3 answers
219 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 ...
user avatar
19 votes
9 answers
391 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 ...
user avatar
16 votes
0 answers
122 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 ...
user avatar
  • 3,720
27 votes
8 answers
420 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
108 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 ...
user avatar
  • 868