Cultural advice

The Australian National University acknowledges, celebrates and pays our respects to the Ngunnawal and Ngambri people of the Canberra region and to all First Nations Australians on whose traditional lands we meet and work, and whose cultures are among the oldest continuing cultures in human history.

Aboriginal and Torres Strait Islander peoples are advised that ANU Library collections may include images, names, voices, and other representations of deceased persons.

Material in the collection may contain terms, language or views that reflect the period in which the item was created and may be considered inappropriate today.

Verified characteristic formulae for CakeML

Simple item page
dc.contributor.authorGuéneau, Armäel
dc.contributor.authorMyreen, Magnus O.
dc.contributor.authorKumar, Ramana
dc.contributor.authorNorrish, Michael
dc.contributor.editorYang, H.
dc.coverage.spatialUppsala, Sweden
dc.date.accessioned2020-12-20T20:58:28Z
dc.date.available2020-12-20T20:58:28Z
dc.date.createdApril 22-29 2017
dc.date.issued2017
dc.date.updated2020-11-23T11:26:24Z
dc.description.abstractCharacteristic Formulae (CF) offer a productive, principled approach to generating verification conditions for higher-order imperative programs, but so far the soundness of CF has only been considered with respect to an informal specification of a programming language (OCaml). This leaves a gap between what is established by the verification framework and the program that actually runs. We present a fullyfledged CF framework for the formally specified CakeML programming language. Our framework extends the existing CF approach to support exceptions and I/O, thereby covering the full feature set of CakeML, and comes with a formally verified soundness theorem. Furthermore, it integrates with existing proof techniques for verifying CakeML programs. This validates the CF approach, and allows users to prove end-to-end theorems for higher-order imperative programs, from specification to language semantics, within a single theorem prover
dc.format.mimetypeapplication/pdfen_AU
dc.identifier.isbn9783662544334
dc.identifier.urihttp://hdl.handle.net/1885/218599
dc.language.isoen_AUen_AU
dc.publisherSpringer
dc.relation.ispartofseries26th European Symposium on Programming, ESOP 2017 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017
dc.sourceLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
dc.titleVerified characteristic formulae for CakeML
dc.typeConference paper
local.bibliographicCitation.lastpage610
local.bibliographicCitation.startpage584
local.contributor.affiliationGuéneau, Armäel, École Normale Supérieure
local.contributor.affiliationMyreen, Magnus O., University of Cambridge
local.contributor.affiliationKumar, Ramana, CSIRO/UNSW
local.contributor.affiliationNorrish, Michael, College of Engineering and Computer Science, ANU
local.contributor.authoruidNorrish, Michael, u4087502
local.description.notesImported from ARIES
local.description.refereedYes
local.identifier.absfor080308 - Programming Languages
local.identifier.ariespublicationa383154xPUB5907
local.identifier.doi10.1007/978-3-662-54434-1_22
local.identifier.scopusID2-s2.0-85018690438
local.type.statusMetadata only

Downloads

Collections

ANU Research Publications

DSpace software copyright © 2002-2026 LYRASIS

abcd