The Open Calculus of Constructions (Part I): An Equational Type Theory with Dependent Types for Programming, Specification, and Interactive Theorem Proving

Mark-Oliver Stehr. The Open Calculus of Constructions (Part I): An Equational Type Theory with Dependent Types for Programming, Specification, and Interactive Theorem Proving. Fundamenta Informaticae, 68(1-2):131-174, 2005. [doi]

Abstract

Abstract is missing.