Indexed and Fibred Structures for Hoare Logic
| Autor: | Uwe Wolter, Alfio Martini, Edward Hermann Häusler |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2020 |
| Předmět: |
General Computer Science
Computer science Fibered knot Hoare logic Type (model theory) Theoretical Computer Science Axiomatic semantics Focus (linguistics) Algebra TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Syntactic category Fibred category TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Mathematics::Category Theory Computer Science::Logic in Computer Science Computer Science::Programming Languages |
| Zdroj: | Electronical Notes in Theoretical Computer Science LSFA |
| Popis: | Indexed 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. publishedVersion |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|