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]
@article{Stehr05,
title = {The Open Calculus of Constructions (Part I): An Equational Type Theory with Dependent Types for Programming, Specification, and Interactive Theorem Proving},
author = {Mark-Oliver Stehr},
year = {2005},
url = {http://iospress.metapress.com/openurl.asp?genre=article&issn=0169-2968&volume=68&issue=1&spage=131},
tags = {source-to-source, programming, type theory, open-source},
researchr = {https://researchr.org/publication/Stehr05},
cites = {0},
citedby = {0},
journal = {Fundamenta Informaticae},
volume = {68},
number = {1-2},
pages = {131-174},
}