Unanswered Questions
22 questions with no upvoted or accepted answers
23
votes
0
answers
571
views
Categorical semantics of Agda
I would like to know the state of the art regarding the categorical semantics of the type theory implemented by Agda — or at least some approximation of that type theory that is amenable to ...
- 3,200
20
votes
0
answers
234
views
What is known about performance bottlenecks in proof assistants?
Background
In my personal experience, the biggest bottleneck to broader adoption of proof assistants (in industry and mathematics) is the effort it takes to engineer proofs. (In lines of code, for ...
- 1,112
13
votes
0
answers
369
views
Unintentionally proven false theorem with type-in-type outside logic and foundations?
We are all familiar with Russell's paradox, and it is known that Per Martin-Löf proved that type-in-type is normalizing and consistent (which is false), by accidentally using an assumption in his meta-...
12
votes
0
answers
169
views
Rules for mutual inductive/coinductive types
Some proof assistants, like Agda and maybe Coq, allow families of mutually defined types, or nested definitions of types, in which some are inductive and others are coinductive. I have no idea what ...
- 3,200
10
votes
0
answers
187
views
Is there a proof assistant (or an embedding) for the (co)end calculus?
A Higher-Order Calculus for Categories describes a system where you can conveniently perform manipulations with categories, functors, Yoneda embeddings etc. An example of the rules is: $$\frac{\Gamma ,...
- 2,846
9
votes
0
answers
309
views
Alternatives to universe levels
All of the type theory based proof assistants that I have seen have an infinite hierarchy of type universes to avoid the type of types being a term of itself. Are there alternative systems which could ...
- 91
6
votes
0
answers
114
views
Is every logical theory embeddable in a dependently typed extensional type theory?
In category theory by the Yoneda embedding every category $\mathcal{C}$ is a subcategory of a category of presheafs $[\mathcal{C}^{\text{op}}, \text{Set}]$. Every category of presheafs is a topos and ...
- 2,868
6
votes
1
answer
198
views
Tools to formally verify programs written in languages supported by the GNU Compiler (GCC)
Is there a website that maintains a list, or is there a list, of tools that support verification of programs written in languages supported by the GCC compiler front ends: C, C++, Objective-C, Fortran,...
- 406
5
votes
0
answers
246
views
Mere propositions and Consistency with Impredicativity, Excluded Middle and Large Elimination
Setup
Current Understanding
I've recently been trying to learn about the interaction of Impredicative Polymorphism, Large Elimination and Excluded Middle (notably, inconsistency). Notably, this is ...
- 73
5
votes
0
answers
95
views
What is the relation of $\lambda^\to$ and $\lambda^{\to\times}$ to cartesian closed categories?
I am learning about the categorical semantics of type theory. I've written some preliminary results in Agda. In particular, I partially proved that the contexts and substitutions of simply-typed ...
- 4,025
4
votes
0
answers
122
views
Proving "proof methods" as theorems in type-theory based proof systems
For example, suppose we have proved associativity of some binary operator $+ : T \to T$ as
add_assoc : forall (x y : T), x + y + z = x + (y + z).
We can thus prove ...
- 41
4
votes
0
answers
107
views
Independence of function extensionality
Who first realized that function extensionality cannot be proved within vanilla MLTT, or some variations of it? Now to my knowledge the simplest way to show this is by syntactic models. But surely ...
- 4,025
3
votes
0
answers
97
views
Limitations of simple type theory proof assistants for undergraduate-level mathematics?
I'm interested in understanding the practical power and limitations of simple type theory, particularly as compared with dependent type theory, in supporting formalized proofs of theorems liable to ...
- 345
2
votes
0
answers
105
views
Algebraic manipulation: what is the best tool?
I have a set of algebraic axioms. I need to prove an equation, an algebraic law. What I did was applying "trivial" rewrite rules by a theorem prover from both ends, and then an automatic ...
- 321
2
votes
0
answers
81
views
Formally verified email or communication?
This question is contextualized by having an account hacked which is prompting me to move towards something I’ve long wanted to anyway.
I would like to consider the simplest possible formally verified ...
