Reasoning about iteration and recursion uniformly based on big-step semantics
From MaRDI portal
Publication:2154025
DOI10.1007/978-3-030-91265-9_4zbMath1498.68077arXiv2108.01883OpenAlexW3216825539MaRDI QIDQ2154025
Qianying Zhang, Yong Guan, Ximeng Li, Guo-hui Wang, Zhiping Shi
Publication date: 13 July 2022
Full work available at URL: https://arxiv.org/abs/2108.01883
Theory of programming languages (68N15) Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Formalization of mathematics in connection with theorem provers (68V20)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Semantics with applications: an appetizer.
- A UTP semantics for \textsf{Circus}
- RCOS: a formal model-driven engineering method for component-based software
- Theoretical and practical approaches to the denotational semantics for MDESL based on UTP
- The \textsc{MetaCoq} project
- Program verification by coinduction
- Mechanized semantics for the clight subset of the C language
- Verified Software Toolchain
- Theories of Programming Languages
- Iris from the ground up: A modular foundation for higher-order concurrent separation logic
- An axiomatic basis for computer programming
- Correct Hardware Design and Verification Methods
This page was built for publication: Reasoning about iteration and recursion uniformly based on big-step semantics
