Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [soundness]

The tag has no usage guidance.

-3
votes
1answer
67 views

Soundness of type (systems)

For someone without strong background in theoretical computer science: can soundness be a property of a type (given a type system), or a property of type systems only? In other words, can we say that ...
30
votes
1answer
989 views

Has a proof checker bug ever invalidated a major proof?

Most (all?) proof assistants have soundness bugs fixed on occasion. However, from those I've seen these bugs are usually difficult to come across unintentionally, and results proved before the bug is ...
11
votes
3answers
670 views

“Guarded” negative occurrences in definition of inductive types, always bad?

I know how some negative occurrences can definitively be bad: ...
9
votes
0answers
109 views

Reference for a propositional proof system being equivalent to its soundness?

I am looking for the original reference for the following statement: Let $P$ be a propositional proof system containing $EF$. Then $P$ is equivalent to $EF+Sound(P)$. Background A propositional ...