Per Martin-Löf. “Constructive mathematics and computer programming”.
In: Logic, Methodology and Philosophy of Science VI. Ed. by L. J. Cohen et al. Amsterdam: North-Holland, 1982, pp. 153-175.
The semantics of the intuitionistic programming language is very close to the semantics presented in this paper. The main differences are that IPL has surjective pairing and that the W type is replaced with the procedure type (denoted by double right arrow in IPL).
Thierry Coquand. “An Algorithm for Type-Checking Dependent Types”.
In: Science of Computer Programming 26 (1996), pp. 167-177.
The algorithm used for type-checking IPL is not much different from the algorithm presented in this paper.
Johan Georg Granström. “A new paradigm for component-based development”.
In: J. Software 7 (2012), pp. 1136-1148.
This paper explains the theoretical foundations for IPL's interfaces and procedures. Note, however, that IPL does not support the full elimination rule for the procedure type, called type of interactive programs in the paper: instead, IPL supports only the operations called “bind” and “lift” in the paper, corresponding to sequential evaluation of programs and for loops in IPL.
Johan Georg Granström. Treatise on Intuitionistic Type Theory.
Logic, Epistemology, and the Unity of Science. Springer, 2011.
In this book, the author explains how intuitionistic type theory can be equipped with eager evaluation semantics. It also contains a wealth of information about the philosophical foundations of intuitionism.
M. Hedberg. “A coherence theorem for Martin-Löf's Type Theory”.
In: J. Funct. Program. 8 (1998), pp. 413-436.
The theorem demonstrated in this paper has been fully implemented in IPL. See the examples section for details.
Other interesting programming languages with dependent types (in alphabetical order):