Recursive Programs as Definitions in First-Order Logic

DOI10.1137/0213026zbMath0559.68020OpenAlexW2049714341MaRDI QIDQ5184385

Robert Cartwright

Publication date: 1984

Published in: SIAM Journal on Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1137/0213026

zbMATH Keywords

verificationprogram transformationssemanticsprogram logicfirst order logichigher order logicrewrite rulesfixed- point theory of recursive programs

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) Higher-type and set recursion theory (03D65) Abstract and axiomatic computability and recursion theory (03D75)

Related Items

Recursive programs and denotational semantics in absolute logics of programs ⋮ What is a universal higher-order programming language? ⋮ Total correctness in nonstandard logics of programs ⋮ Hoare's logic for nondeterministic regular programs: A nonstandard approach

Uses Software

• LCF