CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

HALO: Haskell to Logic through Denotational Semantics

D. Vytiniotis ; S. P. Jones ; Dan Rosén (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Koen Claessen (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers))
Acm Sigplan Notices (0362-1340). Vol. 48 (2013), 1, p. 431-442.
[Artikel, refereegranskad vetenskaplig]

Even well-typed programs can go wrong in modern functional languages, by encountering a pattern-match failure, or simply returning the wrong answer. An increasingly-popular response is to allow programmers to write contracts that express semantic properties, such as crash-freedom or some useful post-condition. We study the static verification of such contracts. Our main contribution is a novel translation to first-order logic of both Haskell programs, and contracts written in Haskell, all justified by denotational semantics. This translation enables us to prove that functions satisfy their contracts using an off-the-shelf first-order logic theorem prover.

Nyckelord: verification, languages, static contract checking, first-order logic

Denna post skapades 2013-06-17. Senast ändrad 2015-07-03.
CPL Pubid: 178613


Läs direkt!

Länk till annan sajt (kan kräva inloggning)

Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)



Chalmers infrastruktur