22 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(...
Andrej Bauer's user avatar
  • 28.9k
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 ...
Andrej Bauer's user avatar
  • 28.9k
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 ...
Neel Krishnaswami's user avatar
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 ...
Jacques Carette's user avatar
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 ...
cody's user avatar
  • 13.9k
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 ...
Martin Berger's user avatar
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....
Martin Hofmann's user avatar
10 votes

Intuitive explanation of the fact that the Calculus of Constructions is not conservative over Higher-Order Logic

I do not know if this answers your question, but in Propositions as [Types] we communicate in Remark 6.6 an observation by Thierry Coquand, namely that the statement $$ (\forall x .\, \exists y .\, R(...
Andrej Bauer's user avatar
  • 28.9k
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/...
Jesper's user avatar
  • 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 ...
Joshua Grochow's user avatar
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.
Martin Berger's user avatar
8 votes

Formal semantics of tactics

Obviously there is an operational semantics of Ltac by Jedynak et al.
xrq's user avatar
  • 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 ...
Neel Krishnaswami's user avatar
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: ...
András Kovács's user avatar
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 ...
Andrej Bauer's user avatar
  • 28.9k
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 ...
Martin Hofmann's user avatar
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 ...
Clément's user avatar
  • 161
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. ...
cody's user avatar
  • 13.9k
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 ...
wren romano's user avatar
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/...
Kaveh's user avatar
  • 21.6k
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.
Michael Norrish's user avatar
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 ...
Neel Krishnaswami's user avatar
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 ...
Noam Zeilberger's user avatar
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 ...
Andrej Bauer's user avatar
  • 28.9k
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 :)
Catalin Hritcu's user avatar
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 ...
Dominic Mulligan's user avatar
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 (...
cody's user avatar
  • 13.9k
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 ...
cody's user avatar
  • 13.9k
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 ...
András Kovács's user avatar
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) $\...
cody's user avatar
  • 13.9k

Only top scored, non community-wiki answers of a minimum length are eligible