22
votes
What should a proof of correctness for a typechecker actually be proving?
That's a good question! It asks what we expect from types in a typed language.
First note that we can type any programing language with the unitype: just pick a letter, say ...
- 28.3k
21
votes
Accepted
Proof relevance vs. proof irrelevance
There are several possible notions of proof relevance. Let us consider three similar situations:
An element of a sum $\Sigma (x : A) . P(x)$ is a pair $(a, p)$ where $a : A$ and $p$ is a proof of $P(...
- 28.3k
15
votes
Accepted
Proof assistant usage in complexity theory research?
A general rule of thumb is that the more abstract/exotic the mathematics you want to mechanise, the easier it gets. Conversely, the more concrete/familiar the mathematics is, the harder it will be. So ...
- 32.4k
14
votes
Proof relevance vs. proof irrelevance
I recommend that everyone first read Andrej Bauer's answer, as he covers all the basics extremely well. I agree with everything he says in his answer. I humbly offer more comments, even though I know ...
- 1,530
11
votes
Accepted
Has a proof checker bug ever invalidated a major proof?
To my knowledge, no machine checked proof of a complex mathematical development has ever been retracted.
As Andrej points out though, it occasionally happens that soundness-breaking bugs do crop up ...
- 13.7k
10
votes
Formally Verified Complexity Theory
In the following paper my colleague Uli Schöpp presents a formal verification (in Coq) of a nontrivial result by Cook and Rackoff on the computational power of graph automata. https://scholar.google....
- 643
10
votes
Accepted
What should a proof of correctness for a typechecker actually be proving?
The question can be interpreted in two ways:
Whether the implementation does implement a given typing system $T$?
Whether the typing system $T$ does prevent the errors you think it should?
The ...
- 11.4k
8
votes
Accepted
Small kernel (i.e. proof-verifier) for Agda?
It is true that Agda currently has a much shakier foundation than say Coq or Lean. It does have an internal term syntax that could be seen as a core language (https://github.com/agda/agda/blob/master/...
- 356
8
votes
Accepted
Is Buchberger's algorithm or Wu's method valuable theoretically when we have the Tarski–Seidenberg theorem?
For Buchberger, it depends what you want it for, but generally speaking the answer is no. First, as pointed out on the Wikipedia article, the complexity upper bound given by Tarski-Seidenberg is ...
- 36.9k
8
votes
Accepted
Formal semantics of tactics
I'm not sure this answers your question, but the first (?) paper on the subject of tactics appears to have been Milner's The Use of Machines to Assist in Rigorous Proof.
- 11.4k
8
votes
Formal semantics of tactics
Obviously there is an operational semantics of Ltac by Jedynak et al.
- 1,175
7
votes
Proving running time upper bounds for algorithms in dependent type theory
As usual, (a) the high-level conceptual approach is basically the same as it is on paper, but (b) mechanization makes new things reasonable to attempt.
The way you do things is to define a cost ...
- 32.4k
7
votes
Accepted
Structural equality of Pi Types with heterogeneous equality?
I am not aware that J or K exists for heterogeneous equality. It does not need an elimination principle, because it can be simply defined as a sigma type:
...
- 1,444
6
votes
Accepted
Why REFL rule is primitive in HOL Light?
DEDUCT_ANTISYM_RULE only applies to propositions, while REFL applies to all terms of all types. Your suggestion only shows that ...
- 28.3k
6
votes
Proof assistant usage in complexity theory research?
One very prominent example is of course Gonthiers Coq formalization of the 4 color theorem in Coq which uses a lot of combinatorics.
My colleague Uli Schöpp used the ssreflect library developed by ...
- 643
6
votes
Formally Verified Complexity Theory
A nice example is Hugo Férée, Samuel Hym, Micaela Mayero, Jean-Yves Moyen, David Nowak:
Formal proof of polynomial-time complexity with quasi-interpretations. CPP 2018: 146-157
Their abstract (my ...
- 161
5
votes
What should a proof of correctness for a typechecker actually be proving?
There are a few different things you could mean by "prove that my typechecker works". Which, I suppose, is part of what your question is asking ;)
One half of this question is proving that your type ...
- 720
5
votes
Where is the quote "Informal proofs are algorithms, formal proofs are code" from?
He doesn't cite any references for it and
Google doesn't return any results so
I don't think he is really quoting from anywhere.
The idea that a proof is a "construction"
(a term in intuitionistic/...
- 21.5k
5
votes
Has the compactness theorem for FOL been formalized in Coq/Isabelle/etc?
Compactness for FOL was done in HOL by John Harrison, and reported at TPHOLs 1998. See Formalizing basic first order model theory.
- 151
5
votes
Accepted
Representations of Planar Graphs in Coq
The obvious resource for planar graphs in Coq would be the (modern port of) the four color theorem in Coq/SSReflect, by Georges Gonthier (and others) which obviously does need to define planar graphs.
...
- 13.7k
4
votes
Representations of Planar Graphs in Coq
I just wanted to make some additional comments not already covered by Cody's nice answer, and also address question (2).
First, Gonthier goes into detail about the representation of planar maps used ...
- 4,431
4
votes
Fixed set of type constructors to simulate all intensional inductive families?
I am not 100% sure this is what you want, but assuming you are looking for a type theory with a closed set of type constructors, which can model inductive families, then what you want are indexed ...
- 32.4k
4
votes
Accepted
Why is plus-comm a b $:\equiv$ refl (plus a b) not a proof of the commutativity of addition?
But it does follow. The types
$$A = \prod_{(n,m:\textrm{Nat})}(\textrm{plus}\ n\ m) = (\textrm{plus}\ n\ m)$$
and
$$B = \prod_{(n,m:\textrm{Nat})}(\textrm{plus}\ n\ m) = (\textrm{plus}\ m\ n)$$
are ...
- 28.3k
4
votes
How would I go about learning the underlying theory of the Coq proof assistant?
The current Software Foundations book does explain all this later on:
https://softwarefoundations.cis.upenn.edu/lf-current/ProofObjects.html
So if you're following the book, just read on :)
- 141
4
votes
Proving running time upper bounds for algorithms in dependent type theory
For verified complexity analysis in other theorem proving systems, see e.g. Tobias Nipkow's paper on this subject using the Isabelle theorem prover ("Amortised Complexity Verified" at ITP 2015) which ...
- 837
4
votes
Proving running time upper bounds for algorithms in dependent type theory
As Neel answered, you can (theoretically) prove anything in a proof assistant that you can prove on paper, including idealized run-times or resource usage for a program modeled using a deep embedding (...
- 13.7k
3
votes
Accepted
Using ϵ -unification and Knuth-Bendix completion to automatically proof theorems about groups
This is going to be a somewhat incomplete answer, since you are asking some pretty broad questions about the applications of the techniques.
First let me start by saying that while the research in ...
- 13.7k
3
votes
Accepted
Is there a theory of overloading types?
As far as I know, there is no "right" or "only" way of associating operations of theorems to mathematical structures. Certainly there is no canonical way, and even on paper you often see sentences ...
- 13.7k
3
votes
Why is plus-comm a b $:\equiv$ refl (plus a b) not a proof of the commutativity of addition?
Addressing the question in the title: $\mathsf{\lambda n\,m.\,refl}$ is not a proof of commutativity by definition because addition is not a constant function by definition. Of course, the ...
- 1,444
2
votes
Accepted
What is the relation of HOL Light type theory and some of the intuitionistic type theories?
There are a number of ways to see HOL as an instance of a "dependent" type theory, in a way that is reasonable, that is there is a pure type system (https://en.wikipedia.org/wiki/Pure_type_system) $\...
- 13.7k
Only top scored, non community-wiki answers of a minimum length are eligible