PML est un langage de programmation en appel par valeurs similaire à ML, avec une syntaxe à la Curry (c'est à dire, pas de types dans les termes) et basé sur une logique d'ordre supérieur classique. Les termes apparaissent dans les types via un prédicat d'appartenance t ∈ A et un opérateur de restriction A | t ≡ u. La sémantique de ces deux constructeurs de types utilise une relation d'équivalence (observationnelle) sur les programmes (non typés). L'opérateur de restriction est utile pour l'écriture de spécifications tandis que l'appartenance permet d'encoder les types dépendants. La présence de l'équivalence nous permet également de relâcher la « value restriction » pour obtenir un type produit dépendant compatible avec la logique classique (ce qui n'avait pas été fait avant).