Rahli, Vincent; Bickford, Mark; Cohen, Liron; Constable, Robert L. Bar induction is compatible with constructive type theory. (English) Zbl 1427.03066 J. ACM 66, No. 2, Article No. 13, 35 p. (2019). Cited in 1 Document MSC: 03F50 Metamathematics of constructive systems 03B38 Type theory 68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) Keywords:bar induction; Coq; Nuprl; W-types; choice sequences; computational type theory; intuitionistic logic; semantics Software:Idris; seL4; Lean; CertiKOS; Nuprl; Coq; Agda PDFBibTeX XMLCite \textit{V. Rahli} et al., J. ACM 66, No. 2, Article No. 13, 35 p. (2019; Zbl 1427.03066) Full Text: DOI