Recursive programs and denotational semantics in absolute logics of programs

DOI10.1016/0304-3975(90)90156-CzbMath0718.03021MaRDI QIDQ2639051

Ana Pasztor

Publication date: 1990

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

denotational semanticsprogram verificationrecursive programsnonstandard logics of programsfirst-order dynamic logicKPU-absolute logic

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Changing a Semantics: Opportunism or Courage?, Some general incompleteness results for partial correctness logics, Is ``Some-other-time sometimes better than ``Sometime for proving partial correctness of programs?, On the strength of temporal proofs

Cites Work

• Total correctness in nonstandard logics of programs
• A completeness theorem for dynamic logic
• A simple proof for the completeness of Floyd's method
• Some questions about expressiveness and relative completeness in Hoare's logic
• Non-standard algorithmic and dynamic logic
• A simple dynamic logic
• Concerning some cylindric algebra versions of the downward Löwenheim- Skolem theorem
• Weak second order characterizations of various program verification systems
• A complete logic for reasoning about programs via nonstandard model theory. II
• Programs and program verifications in a general setting
• LCF considered as a programming language
• First-order dynamic logic
• On the strength of “sometimes” and “always” in program verification
• STRUCTURED NONSTANDARD DYNAMIC LOGIC
• A PROPERTY OF 2‐SORTED PEANO MODELS AND PROGRAM VERIFICATION
• On the termination of program schemas
• The denotational semantics of programming languages
• Recursive Programs as Definitions in First-Order Logic
• Completeness in the theory of types
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item