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

Andrei Paskevich 1
1 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : 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.
Document type :
Reports
[Research Report] RR-7128, INRIA. 2009
Liste complète des métadonnées

Cited literature [5 references]  Display  Hide  Download

https://hal.inria.fr/inria-00439232
Contributor : Andrei Paskevich <>
Submitted on : Friday, May 28, 2010 - 5:59:04 PM
Last modification on : Thursday, February 9, 2017 - 3:51:50 PM
Document(s) archivé(s) le : Monday, October 22, 2012 - 12:45:44 PM

Files

RR-7128.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00439232, version 2

Collections

Citation

Andrei Paskevich. Algebraic types and pattern matching in the logical language of the Why verification platform. [Research Report] RR-7128, INRIA. 2009. 〈inria-00439232v2〉

Share

Metrics

Record views

247

Document downloads

124