×

Bar induction is compatible with constructive type theory. (English) Zbl 1427.03066


MSC:

03F50 Metamathematics of constructive systems
03B38 Type theory
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)

Software:

Idris; seL4; Lean; CertiKOS; Nuprl; Coq; Agda
PDFBibTeX XMLCite
Full Text: DOI