Based on these ideas, Barthe and others defined classical pure type systems (CPTS) by adding a double negation operator.
Βασισμένος σε αυτές της ιδέες, ο Barthe και άλλοι όρισαν τα κλασικά αμιγή συστήματα τύπων προσθέτοντας έναν τελεστή διπλής άρνησης.