Substructural logic and partial correctness

DOI10.1145/772062.772066zbMath1365.68327OpenAlexW2141931064MaRDI QIDQ5267434

Dexter Kozen, Jerzy Tiuryn

Publication date: 13 June 2017

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/772062.772066

zbMATH Keywords

sequent calculuslinear logicsubstructural logicdynamic logicspecificationHoare logicKleene algebraKleene algebra with tests

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Structure of proofs (03F07) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47)

Related Items (7)

Concurrent Kleene algebra with tests and branching automata ⋮ Left-Handed Completeness ⋮ Embedding Kozen-Tiuryn logic into residuated one-sorted Kleene algebra with tests ⋮ Local variable scoping and Kleene algebra with tests ⋮ Sequential dynamic logic ⋮ Left-handed completeness ⋮ KAT-ML: an interactive theorem prover for Kleene algebra with tests

This page was built for publication: Substructural logic and partial correctness