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
18
votes
Accepted
Yet another constructive (Coq) proof that `nat -> nat -> nat` is not bijective. How to explain it to myself?
First, let me say that "constructive" does not imply "all maps are Turing computable". It means “no excluded middle and axiom of choice were used“. In constructive mathematics the ...
- 28.3k
14
votes
Accepted
Defining inductive types in intensional type theory purely in terms of type-theoretic data
It turns out that $W$ types plus identity types (eq/= in Coq) allow you to construct pretty much all the general inductive types ...
- 256
12
votes
Formal semantics of OCaml in Coq
Have you seen Arthur Charguéraud's PhD thesis, Characteristic Formulae for Mechanized Program Verification?
Rather than building the type system and small-step semantics as inductive relations, he ...
- 32.4k
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
10
votes
Accepted
What exactly is "large elimination"?
You are incorrect about the definition of large elimination: it refers to the ability to build values of type $\mathrm{Type}$ by eliminating an inductive value. The canonical example:
...
- 13.7k
9
votes
Accepted
Examples of Universe inconsistency in normal use of dependent types
This is a hard question to answer, in part because it's unclear what it means to get something "by accident". Regularly, though, people run into the ...
- 13.7k
8
votes
Accepted
Is there a formalization of normalization of impredicative system F?
Coq without Prop is not strong enough, because it's basically Martin-Löf type theory with universes.
Coq with Prop is strong enough, because you can encode sets of normalizing terms via predicates $S :...
- 32.4k
8
votes
Formal semantics of OCaml in Coq
You could be interested in Jacques Garrigue's A Certified Implementation of ML with Structural Polymorphism and Recursive Types, which establishes the soundness of static and dynamic semantics and ...
- 2,040
6
votes
Accepted
Impredicativity + large eliminations (with no excluded middle) in Coq
No: strong elimination of large inductive types (SELIT) is itself inconsistent because it breaks the layering of universes by trivially allowing you to smuggle a large value in a Prop box and take it ...
- 390
6
votes
Accepted
Defining finite sets inductively in a proof assistant?
There are many variants of finite sets in constructive mathematics. One that can be defined using just inductive definitions, and is therefore amenable to formalization in type theory, is the ...
- 28.3k
6
votes
Accepted
How does axiom K contradict univalence?
You will certainly find it natural that most types, like structures, admit different isomorphisms. Just take the type $\textbf{2}$, with inhabitants $0_\textbf{2}$ and $1_\textbf{2}$. It admits 2 ...
- 176
6
votes
Accepted
Formalization of matching logic (logic behind K Framework)
There is a number of formalizations of matching logic in various proof assistants. I am a co-author of the first one in the following list; thus I have more insight into that one. I am not aware of ...
- 176
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
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
5
votes
Accepted
Universe polymorphism: the inference of universes and their constraints
It's complicated because universe constraints are simplified during inference (in order to avoid an explosion of constraints). Have a look at:
Matthieu Sozeau and Nicolas Tabareau: Universe ...
- 28.3k
5
votes
Accepted
`f_equal` isn't doing anything
The f_equal tactic does not do anything because what you are trying to prove is not true. You assumed that the first components (...
- 28.3k
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
4
votes
Dependent eliminator for empty type in intensional Martin-Löf type theory
$\text{absurd} : (A : \text{U}) \to 0 \to A$ and $\text{elim} : (A : 0 \to \text{U}) \to (x : 0) \to A\,x$ are equivalent. To go right, use $\text{absurd}\,(A\,x)\,x$. To go left, use $\text{elim}\,(\...
- 1,444
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
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
How can you build a coinductive memoization table for recursive functions over binary trees?
It's easy enough to get the recursion pattern to work with sized types.
Hopefully the sharing is preserved through compilation![1]
...
- 141
3
votes
What exactly is "large elimination"?
Here is another attempt to illustrate large elimination. Consider the two following two ways to define a type: as an inductive or by induction.
For instance, here are two definitions of a vector with ...
- 31
3
votes
Featherweight Generic Java formalization in Coq
I guess somewhat more realistic task would be to find Coq's formalisation of FJ itself (probably with some extensions, but not necessarily FGJ). The one which I googled easily is:
Encoding ...
- 1,093
3
votes
Modeling objects (OOP) in dependent type theory
There is a substantially expanded follow paper Andreas Abel, Stephan Adelsberger, Anton Setzer: Interactive Programming in Agda -
Objects and Graphical User Interfaces. It contains an Agda library ...
- 31
3
votes
2
votes
Why does Coq have Prop?
The principle of propositions-as-types (or formulas-as-types), also known as the Curry-Howard correspondence, is the key idea for viewing (intuitionistic) type theories as logical systems and to apply ...
- 21
2
votes
How does axiom K contradict univalence?
For a quick reference, here's (equation 8) a proof sketched in Agda. But I guess you're asking for the idea, and I think the reference is kinda technical.
When you say 'univalence', you not only mean ...
- 965
1
vote
Yet another constructive (Coq) proof that `nat -> nat -> nat` is not bijective. How to explain it to myself?
To answer very directly: You have a constructive proof in Coq but it is not the case that the enum : nat -> nat is assumed (in Coq) to be computable. In a sense, ...
- 11
1
vote
Accepted
A Coq question : How to prove the image of the two same valued variables under a function are same?
You can't do that.
You can actually define a function which doesn't respect Q's setoid structure.
...
Only top scored, non community-wiki answers of a minimum length are eligible