# Questions tagged [coq]

Coq is an interactive theorem prover.

12 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
0answers
229 views

### Model of Coq (pCuIC) in higher toposes?

Can the type theory of Coq (pCuIC) be modeled in all higher Grothendieck toposes? First of all, even the set theoretical model is not complete (e.g. inductive types in Prop). Although, this is ...
0answers
503 views

### An axiom for John Major's Equality

In the the standard library of Coq, there is the axiom: Axiom JMeq_eq : forall (A:Type) (x y:A), JMeq x y -> x = y. Why isn't it provable? Can it be reduced ...
0answers
149 views

### On the interpretation of coinduction in type theory

The notion of (co)datatype can be modeled satisfactorily in category theory as fixed-points of polynomial functors. Then, (co)induction principles are derived from initial algebras/terminal ...
0answers
123 views

### major applied focuses of different proof assistants

Currently, what are the major applied focuses (if any applications can be deserved such a distinction) of different proof assistants, such as the following? If there are significant differences ...
0answers
123 views

### Have the proofs in Buss's “On Goedel’s Theorems on Lengths of Proofs” been formalized (mechanically checked)?

The paper On Gödel's theorems on lengths of proofs I: Number of lines and speedup for arithmetics contains quite interesting results on proof length. But some of the details are still, to me, a bit ...
0answers
169 views

### Type theoretic equivalent of isomorphism class

How one defines the notion of isomorphism class in type theory? For concreteness I will describe what I mean with an example in Coq. Suppose I have a record ToyRec: ...
0answers
359 views

### Encoding a logic in Coq

I want to encode a logic into Coq. The semantics of the logic are very complex and I just want to encode the syntax, axioms, inference rules. I use deep embedding, but I can't use notation like: <...
0answers
72 views

### Journals or conferences to submit formally verified libraries?

This is a soft question aimed at understanding whether there is any value to publishing formally verified libraries. I have formally verified (in Coq) implementations of: synthetic differential ...
0answers
257 views

### Is it possible to type Ackermann function with (stratified variant of) System F?

I was surprised to find no open-source implementation of Ackermann function in pure System F as an illustrative example. I finally managed to implement it myself in Haskell using Church encoding: <...
0answers
73 views

### What do we call a type system where any term of any type ultimately parses down to $*:\mathbf{1}$?

If a type system allows inductive types (as in e.g. Coq) then we can coin new primitive constants that inhabit types. For example $0:\mathbb{N}$ is constructed when defining $\mathbb{N}$ and does not ...
0answers
78 views

### Proposition terms vs types in Coq

Consider the following div function written in Coq. It takes in a proof that the divider is non-zero. Definition div (n d:nat) (pf: ~(d = 0)) := n/d. Focus on <...
1answer
254 views

### Problem in embedding

I want to embed PPTL(a kind of logic) in Coq. Because of its complex semantics, I just embed its systax. ...