jats-ug/translate — pull request #6 by dif-engine (2014-06-14 03:01:35+00:00)
Title: Update SPPSV-padl05.md

We adopt a light-weighted approach, introducing a notion of restricted form of dependent
types, where we clearly separate type index expressions from run-time expressions.
In functional programming, we have enriched the type system of ML with such
a form of dependent types, leading to the design of a functional programming language
DML (Dependent ML) [Xi98,XP99].In imperative programming, we have designed a
programming language Xanadu with C-like syntax to support such a form of dependent
types.

の訳文