Search type Search syntax
Tags [tag]
Exact "words here"
Author user:1234
user:me (yours)
Score score:3 (3+)
score:0 (none)
Answers answers:3 (3+)
answers:0 (none)
Views views:250
Code code:"if (foo != bar)"
Sections title:apples
body:"apples oranges"
URL url:"*"
Saves in:saves
Status closed:yes
Types is:question
Exclude -[tag]
For more details on advanced search visit our help page
Results tagged with
Search options not deleted user 14

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

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 awa …
  • 1,439
2 votes

Reference request for an introduction to higher-order logic

I found it useful to also read books on higher-order logic, several I can recommend: Stewart Shapiro, Foundations without foundationalism (which argues second-order logic is adequate for doing ordina …
  • 1,439
10 votes

What are good books for learning about proof assistants for Functional Analysis?

The question could be summed up as a request for resources about formalizing functional analysis in proof assistants. For this, I would recommend: Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia M …
  • 1,439
18 votes

Where can I find lists of theorems that have been verified?

Mizar publishes them quarterly in their journal Formalized Mathematics.
7 votes

PDEs and proof assistants

A fragment of traditional PDE theory has been formalized in Mizar: Sora Otsuki and Pauline N. Kawamoto and Hiroshi Yamazaki, "A Simple Example for Linear Partial Differential Equations and Its Soluti …
  • 1,439