Extending higher-order logic with predicate subtyping : application to 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 critères plus complexes comme l'absence de divisions par zéro. Cette thèse...

Full description

Bibliographic Details
Main Author: Gilbert, Frédéric
Other Authors: Sorbonne Paris Cité
Language:en
Published: 2018
Subjects:
Online Access:http://www.theses.fr/2018USPCC009/document