Algebraic types and pattern matching in the logical language of the Why verification platform - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2009

Algebraic types and pattern matching in the logical language of the Why verification platform

Andrei Paskevich (1)
Andrei Paskevich
Proof of Programs
CV

Résumé

We introduce an extension of the logical language of a software verification tool Why with algebraic types and pattern matching expressions. We describe the corresponding additions to the syntax of Why and give the semantics of the new constructions in terms of first-order logic with polymorphic types as it is adopted in Why and the Alt-Ergo prover.

Domaines

Logique en informatique [cs.LO]
Fichier principal
Vignette du fichier
RR-7128.pdf (317.22 Ko) Télécharger le fichier
Vignette du fichier
sshot.png (131.49 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Format : Figure, Image

Andrei Paskevich  : Connectez-vous pour contacter le contributeur

https://inria.hal.science/inria-00439232

Soumis le : lundi 7 décembre 2009-03:06:20

Dernière modification le : mardi 19 septembre 2023-13:26:03

Archivage à long terme le : jeudi 17 juin 2010-23:20:27

Télécharger pour visualiser

Dates et versions

inria-00439232 , version 1 (07-12-2009)
inria-00439232 , version 2 (28-05-2010)

Identifiants

  • HAL Id : inria-00439232 , version 1

Citer

Andrei Paskevich. Algebraic types and pattern matching in the logical language of the Why verification platform. [Research Report] RR-7128, 2009. ⟨inria-00439232v1⟩

Exporter

BibTeX XML-TEI Dublin Core DC Terms EndNote DataCite

Collections

INRIA-RRRT
190 Consultations
148 Téléchargements

Partager

Gmail Facebook X LinkedIn More