Hacker News
new
|
past
|
comments
|
ask
|
show
|
jobs
|
submit
login
CHY872
on March 25, 2015
|
parent
|
context
|
favorite
| on:
Proving false in Coq using an implementation bug
> Actually, I am aware of another, much more serious problem with CoIC formalism which was found when Coq was tried to be used to formalize homotopy type theory. It was a bug in CoIC, not a software bug.
Do you have any references? Intrigued :)
vilhelm_s
on March 25, 2015
[–]
The notion of guardedness (for structural recursion) was a bit too permissive. This lead to inconsistency if you assume e.g. (False->False = True) (which is implied by propositional extensionality, and by the univalence axiom). The same issue affected Agda also. It was discussed a lot on the Coq and Agda mailing lists, e.g.
https://sympa.inria.fr/sympa/arc/coq-club/2013-12/msg00119.h...
http://agda.chalmers.narkive.com/E2UeRTOx/re-coq-club-propos...
Guidelines
|
FAQ
|
Lists
|
API
|
Security
|
Legal
|
Apply to YC
|
Contact
Search:
Do you have any references? Intrigued :)