Vis enkel innførsel

dc.contributor.authorWolter, Uwe Egbert
dc.contributor.authorMartini, Alfio
dc.contributor.authorHaeusler, Edward Hermann
dc.date.accessioned2021-06-28T11:06:24Z
dc.date.available2021-06-28T11:06:24Z
dc.date.created2021-01-29T23:37:43Z
dc.date.issued2020
dc.PublishedElectronical Notes in Theoretical Computer Science. 2020, 348 125-145.
dc.identifier.issn1571-0661
dc.identifier.urihttps://hdl.handle.net/11250/2761610
dc.description.abstractIndexed and fibred categorical concepts are widely used in computer science as models of logical systems and type theories. Here we focus on Hoare logic and show that a comprehensive categorical analysis of its axiomatic semantics needs the languages of indexed category and fibred category theory. The structural features of the language are presented in an indexed setting, while the logical features of deduction are modeled in the fibred one. Especially, Hoare triples arise naturally as special arrows in a fibred category over a syntactic category of programs, while deduction in the Hoare calculus can be characterized categorically by the heuristic deduction = generation of cartesian arrows + composition of arrows.en_US
dc.language.isoengen_US
dc.publisherElsevieren_US
dc.rightsAttribution-NonCommercial-NoDerivatives 4.0 Internasjonal*
dc.rights.urihttp://creativecommons.org/licenses/by-nc-nd/4.0/deed.no*
dc.titleIndexed and Fibred Structures for Hoare Logicen_US
dc.typeJournal articleen_US
dc.typePeer revieweden_US
dc.description.versionpublishedVersionen_US
dc.rights.holderCopyright 2020 The Authorsen_US
cristin.ispublishedtrue
cristin.fulltextoriginal
cristin.qualitycode1
dc.identifier.doihttps://doi.org/10.1016/j.entcs.2020.02.008
dc.identifier.cristin1883078
dc.source.journalElectronical Notes in Theoretical Computer Scienceen_US
dc.source.40348
dc.source.pagenumber125-145en_US
dc.identifier.citationElectronical Notes in Theoretical Computer Science. 2020, 348, 125-145en_US
dc.source.volume348en_US


Tilhørende fil(er)

Thumbnail

Denne innførselen finnes i følgende samling(er)

Vis enkel innførsel

Attribution-NonCommercial-NoDerivatives 4.0 Internasjonal
Med mindre annet er angitt, så er denne innførselen lisensiert som Attribution-NonCommercial-NoDerivatives 4.0 Internasjonal