Inductive Construction in Nuprl Type Theory Using Bar Induction
by Mark Bickford, Robert L. Constable
2014
Presented at TYPES 2014: Types for Proofs and Programs, in Paris, France.
Presented at TYPES 2014: Types for Proofs and Programs, in Paris, France.