Compatibility of impredicative Set and function extensionality
Compatibility of impredicative Set and function extensionality
coq
Differences between Coq and Agda
Coq has been designed with theorem proving in mind, whereas Agda has been designed with dependently-typed programming in mind. They are somewhat equivalent on the theoretical side (even though they have differences, Coq being slightly more conservative in its axioms and sticking closer to the mathematical foundation of CIC by default), but I would trust … Read more
Difference between type parameters and indices?
When you see a family of types, you may wonder whether each of the arguments it has are parameters or indices. Parameters are merely indicative that the type is somewhat generic, and behaves parametrically with regards to the argument supplied. What this means for instance, is that the type List T will have the same … Read more
How do we overcome the compile time and runtime gap when programming in a Dependently Typed Language?
Suppose we input n :: Int at runtime from STDIN. We then read n strings, and store them into vn :: Vect n String (pretend for the moment this can be done). Similarly, we can read m :: Int and vm :: Vect m String. Finally, we concatenate the two vectors: vn ++ vm (simplifying … Read more
Difference between Z3 and coq
Coq is an interactive theorem prover (aka proof assistant). It provides a language to write mathematical definitions, algorithms and theorems. It also provides an environment for producing machine checked proofs. Coq has been used to formalize mathematical theorems, and provide the semantics of programming languages. Today, we can find many papers at POPL that used … Read more
What are the practical limitations of a non-turing complete language like Coq?
First, I assume you’ve already heard of the Church-Turing thesis, which states that anything we call “computation” is something that can be done with a Turing machine (or any of the many other equivalent models). So a Turing-complete language is one in which any computation can be expressed. Conversely, a Turing-incomplete language is one in … Read more
Why is my definition not allowed because of strict positivity?
Unfortunately, there’s nothing super deep about this example. As you noted Agda accepts it, and what trips Coq is the lack of uniformity in the parameters. For example, it accepts this: Inductive SwitchNSPA (A : Type) : Type := | switchNSPA : SwitchNSPA A -> SwitchNSPA A. Inductive UseSwitchNSPA := | useSwitchNSPA : SwitchNSPA UseSwitchNSPA … Read more
What are the strengths and weaknesses of the Isabelle proof assistant compared to Coq?
I am mostly familiar with Coq, and do not have much experience with Isabelle/HOL, but I might be able to help a little bit. Perhaps others with more experience on Isabelle/HOL can help improve this. There are two big points of divergence between the two systems: the underlying theories and the style of interaction. I’ll … Read more