Extending higher-order logic with predicate subtyping : application to PVS

Extension de la logique d'ordre supérieur avec le sous-typage par prédicats : application à PVS Le système de types de la logique d'ordre supérieur permet d'exclure certaines expressions indésirables telles que l'application d'un prédicat à lui-même. Cependant, il ne suffit pas pour vérifier des cri... View More